| Commit message (Collapse) | Author | Age |
|
|
|
| |
does not print to ** which is a keyword.
|
|
|
|
|
|
|
|
|
| |
It has been accidentaly broken since early 2014 (and especially
in 8.5), no easy repair, I won't devote any more hours to this stuff.
Moreover no one seems to care apart from Emilio, but he's ok to work
on this in a separate repository or branch.
I left a dev/doc/ocamlbuild.txt file with a few words about this
experiment.
|
| |
|
|
|
|
| |
and global for 8.4 and 8.5.
|
| |
|
|\ |
|
| |
| |
| |
| |
| |
| | |
Note that this breaks the compatibility, in a beneficial way I believe. Tactics
defined in strict mode (i.e. through Ltac foo := ...) may not do an introduction
on a local identifier anymore. They must use the "fresh" primitive instead.
|
|\ \ |
|
| | |
| | |
| | |
| | | |
there is actually no change in default subst between 8.4 and 8.5.
|
|\| | |
|
| | | |
|
|\| | |
|
| | | |
|
| |\ \
| | | |
| | | |
| | | | |
into v8.5
|
|\| | | |
|
| | | |
| | | |
| | | |
| | | | |
This reverts commit c4d1e3113f77af2e5474fe5676c272050dd445e5.
|
| | | |
| | | |
| | | |
| | | | |
This reverts commit 5bed8869b90510f719dcaa5e365b81c6309bdfff.
|
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
the levels."
This reverts commit b6db76517b9a7f21078ab59a0b8eeee6bfdf5ba7.
|
| | | |
| | | |
| | | |
| | | | |
This reverts commit 3a2753bedf43a8c7306b1b3fc9cb37aafb78ad7a.
|
| | | |
| | | |
| | | |
| | | | |
"exists c1, c2".
|
| | | | |
|
| | | |
| | | |
| | | |
| | | | |
implicit is found whether one writes (sig P) or {x|P x}.
|
| | | |
| | | |
| | | |
| | | | |
does not print to ** which is a keyword.
|
| | | | |
|
|\| | | |
|
| | | | |
|
| | | |
| | | |
| | | |
| | | |
| | | | |
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
| | | |
| | | |
| | | |
| | | |
| | | | |
I introduced this bug in 4c078b0362542908eb2fe1d63f0d867b339953fd;
Coq.Init.Notations.constructor does not take any arguments.
|
| | | |
| | | |
| | | |
| | | | |
We no longer need to redefine `refine` (it now shelves by default). Also clean up `constructor` a bit.
|
| | | | |
|
|\ \ \ \
| | | | |
| | | | |
| | | | | |
into JasonGross-trunk-function_scope
|
|\ \ \ \ \
| | |/ / /
| |/| | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
The user-provided sort was ignored for them.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
File contributed by Cédric Auger (a long time ago, sorry!)
Qarith and Qc would probably deserve many more results like this one,
and a more modern style (for instance qualified names), but this commit
is better than nothing...
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
|\| | | | |
|
| | | | | |
|
|\| | | | |
|
| | | | |
| | | | |
| | | | |
| | | | | |
variables and definitions in sections is unsupported.
|
|\| | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The length of the pattern should now be exactly the number of
assumptions and definitions introduced by the destruction or induction,
including the induction hypotheses in case of an induction.
Like for pattern-matching, the local definitions in the argument of
the constructor can be skipped in which case a name is automatically
created for these.
|
| | | | | |
|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
enough
In particular, its interface might still change (in interaction with interested
colleagues). So let's not give it too much visibility yet. Instead, I'll turn
it as an opam packages for now.
|
| |_|_|/
|/| | |
| | | |
| | | | |
Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4.
|
|\| | | |
|