| Age | Commit message (Collapse) | Author |
|---|
|
Small refactoring to pass the `sigma` functionally.
|
|
Equation's terminator had exactly duplicated the shrink function used
in `Abstract`, we remove this duplicity.
|
|
We add the and routine the regular proof save path of Equations was
using.
I don't understand what is going on here, these are a few remarks:
- Equations does capture `sigma` at the time of `start_dependent_lemma`
- A custom hook is also captured, along with telescopes
- The shrink function seems like a duplicate with things already in Coq's
[abstract.ml / declareObl.ml]
I guess the preferred option would be to merge this with the
obligations save path; but I need help from experts.
|
|
Just a cleanup, should bring no functional code change.
|
|
We radically redesign how proof closing information is stored. Instead
of a user-defined closure, we now reify control into a single data
structure containing the needed information.
In this scheme, the `Lemmas` module can get extra information with
obligation info when opening the proof, and will correspondingly call
the right closing function based on this.
This is the start of what could be a much bigger unification of all
the proof save paths.
|
|
This way both `Lemmas` and `DeclareObl` can depend on it, removing one
more difficulty on the unification of terminators.
|
|
This makes the type of terminator simpler, progressing towards its
total reification.
|
|
We move obligation declaration-specific functions to their own
file. This way, `Lemmas` can access them, and in the next part we can
factorize common parts in the save proof.
|
|
As of now, hooks were stored in the terminators as closures, we place
them instead in the proof object and are thus passed back at proof
closing time.
This helps towards the reification and unification of terminators.
|
|
differ in term and type
Reviewed-by: ejgallego
Ack-by: jashug
|
|
Reviewed-by: cpitclaudel
|
|
same thing.
Reviewed-by: ejgallego
|
|
|
|
This is to prevent confusion with the terminology used in the grammar
of tactic in the reference manual: "intropattern" in Tactic Notation
and TACTIC EXTEND is actually bound to simple_intropattern and not to
what is called intropattern in the reference manual
After some deprecation phase, "intropattern" could be added back to
mean the "intropattern" of the reference manual.
Note that "simple_intropattern" is actually already available in
"Tactic Notation" with the correct meaning as an entry. Only
"intropattern" is misguiding.
|
|
Unfortunately, "+" regular expressions are not supported by default
with MacOS X's sed.
It is told that it would work with option -E though, but the syntax
seems then different.
|
|
The ML wrapper was wrongly calling induction instead of destruct.
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
subsequent work.
Reviewed-by: maximedenes
|
|
courtesy)
- index errors (negative or out of bounds) generally throw (panic)
- hd, last, find backtrack, because here backtracking can actually be useful
added a _throw variant to these functions which panics
This emaphasizes the difference between backtracking and throwing exceptions, which doesn't exist in OCaml.
- simplified the implementation of for_all2 and exist2 (ok, that is a matter of taste ...)
- added assertions which combine a boolean match with a throw.
This makes the code more readable and makes it easier to have more specific error messages.
- added a lastn function
- gave Out_of_bounds a message argument (there is no good reason why invalid_argument has one and this not)
All other exceptions without message argument are quite specific to certain functions (like Not_Found)
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: cpitclaudel
|
|
This allows to refer to them from other part of the manual without any ambiguity.
|
|
Reviewed-by: cpitclaudel
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: cpitclaudel
|
|
Reviewed-by: cpitclaudel
|
|
From the CHANGES file in branch v8.9.
|
|
|
|
|
|
Ack-by: ejgallego
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
Reviewed-by: vbgl
|
|
CoqIDE.
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Instead we get the symbols from a Environ.env.
We make them accessible to the produced code through a reference
managed by the kernel, similar to the return values except inverting
when it's written and when it's read.
|
|
Reviewed-by: Zimmi48
|
|
definitions
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ggonthier
Reviewed-by: herbelin
|
|
This also makes vernacentries correct wrt update_global_env.
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
We move the role data into the evarmap instead.
|
|
Reviewed-by: ejgallego
|
