Skip to content

A subtle bug in tclWITHHOLES.#693

Merged
coqbot merged 1 commit into
rocq-prover:v8.6from
herbelin:v8.6+fix-set-evars-theo-bug
May 30, 2017
Merged

A subtle bug in tclWITHHOLES.#693
coqbot merged 1 commit into
rocq-prover:v8.6from
herbelin:v8.6+fix-set-evars-theo-bug

Conversation

@herbelin

Copy link
Copy Markdown
Member

This fixes bug noticed by Théo on tactic set (see #248).

This fixes Théo's bug on eset.
@herbelin herbelin force-pushed the v8.6+fix-set-evars-theo-bug branch from dc4a800 to 1a169b0 Compare May 28, 2017 16:41
@herbelin

Copy link
Copy Markdown
Member Author

Failed with "The job exceeded the maximum time limit for jobs, and has been terminated."

@Zimmi48

Zimmi48 commented May 28, 2017

Copy link
Copy Markdown
Member

@herbelin Are you sure that you are talking about this PR? If yes, did you restart the full build? You could have restarted just the job that failed.

@SkySkimmer

Copy link
Copy Markdown
Contributor

@maximedenes maximedenes reopened this May 28, 2017
@maximedenes

Copy link
Copy Markdown
Member

Travis succeeded, so the compatibility looks good.

I'm not so sure about the code, may @ppedrot can have a quick look?

@maximedenes maximedenes requested a review from ppedrot May 29, 2017 20:59

@ppedrot ppedrot left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM.

@coqbot coqbot merged commit 1a169b0 into rocq-prover:v8.6 May 30, 2017
@Zimmi48 Zimmi48 added the kind: fix This fixes a bug or incorrect documentation. label Jul 21, 2017
@Zimmi48 Zimmi48 added this to the 8.6.1 milestone Jul 21, 2017
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

kind: fix This fixes a bug or incorrect documentation.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

6 participants