[leminv] [declare] Use higher-level Declare API.#12610
Merged
ppedrot merged 2 commits intorocq-prover:masterfrom Sep 18, 2020
Merged
[leminv] [declare] Use higher-level Declare API.#12610ppedrot merged 2 commits intorocq-prover:masterfrom
ppedrot merged 2 commits intorocq-prover:masterfrom
Conversation
ejgallego
commented
Jun 30, 2020
| add_inversion_lemma ~poly na env sigma c sort bool tac | ||
| with | ||
| | UserError (Some "Case analysis",s) -> (* Reference to Indrec *) | ||
| user_err ~hdr:"Inv needs Nodep Prop Set" s |
Contributor
Author
There was a problem hiding this comment.
Note: this was dead code.
Contributor
|
For your complete information, the following job in allow failure mode has failed: test-suite:4.12+trunk+dune |
Contributor
|
For your complete information, the following job in allow failure mode has failed: test-suite:4.11+trunk+dune |
Contributor
|
For your complete information, the following job in allow failure mode has failed: test-suite:base+async |
Contributor
|
check_evars_are_solved is too strict, we only care about the evars in the current definition. |
Contributor
Contributor
Author
ejgallego
force-pushed
the
proof+leminv_ref
branch
from
39e57a0 to
6a9e996
Compare
SkySkimmer
reviewed
Aug 31, 2020
ejgallego
force-pushed
the
proof+leminv_ref
branch
from
6a9e996 to
46c0ad2
Compare
ppedrot
approved these changes
Sep 1, 2020
ejgallego
force-pushed
the
proof+leminv_ref
branch
from
46c0ad2 to
38229bf
Compare
Member
|
Anybody understanding the errors spitted by coq_tools? |
Contributor
Author
Spurious / unrelated so far, let's rerun just in case. |
ejgallego
force-pushed
the
proof+leminv_ref
branch
from
38229bf to
9cc65e5
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Nit on using the higher-level API + bugfix for Derive API.