| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
This closes #6598
|
| |\ |
|
| | | |
|
| |/ |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
| |
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607).
PR #220 put the exports in the wrong compat files, presumably because it
was originally targeted to version 8.6, and this wasn't updated when it
was retargeted to version 8.7.
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
| |/ |
|
| |
|
|
| |
automatically instead
|
| |\
| |
| |
| | |
Was PR#331: Solve_constraints and Set Use Unification Heuristics
|
| | | |
|
| | |
| |
| |
| | |
Some options are expected to be deprecated
|
| |/ |
|
| |
|
|
| |
I've messed up with parts of the compatibility files I had to commit.
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
| |
Since edb55a94fc5c0473e57f5a61c0c723194c2ff414 landed, compat notations
no longer modify the parser in non-compat-mode, so we can do this
without breaking Ltac parsing. Also update the related test-suite
files.
|
| | |
|
| |
|
|
|
|
| |
Importing VectorNotations breaks `; []`. So we make sure it's not
imported by defualt. Some files might be required to `Import
VectorDef.VectorNotations` rather than just `Import VectorNotations`.
|
| |
|
|
|
| |
Also delimit vector_scope with vector, so that people can write %vector
without having to delimit it themselves.
|
| | |
|
| |
|
|
|
|
| |
Add a boolean for refolding during reduction, and an option
that is off by default in 8.6, to turn refolding on in all reduction
functions, as in 8.5.
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
We add a flag Keep Admitted Variables that allows to recover the legacy
v8.4 behaviour of admitted lemmas. The statement of such lemmas did not
depend on the current context variables.
|
| |\| |
|
| | |
| |
| |
| | |
We also add a Coq86.v compat file.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
We don't actually need to, unless we want to support the (presumably
uncommon) use-case of someone using [Import VectorNotations] to override
their local notation for things in vector_scope.
Additionally, we now maintain the behavior that [Import VectorNotations]
opens vector_scope.
|
| | |
| |
| |
| | |
For compatibility with 8.5.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
There were three versions of injection:
1. "injection term" without "as" clause:
was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
was introduction hypotheses using ipat in reverse order without
checking that the number of ipat was the size of the injection
(activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
was introduction hypotheses using ipat in left-to-right order
checking that the number of ipat was the size of the injection
and clearing the injecting term by default if an hypothesis
(activated with "Set Injection L2R Pattern Order", default one from 8.5)
There is now:
4. "injection term" without "as" clause, new version:
introducing the components of the injection in the context in
left-to-right order using default intro-patterns "?"
and clearing the injecting term by default if an hypothesis
(activated with "Set Structural Injection")
The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
introducing the hypotheses in the goal what corresponds to the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
natural expectation as the changes I made in the proof scripts for
adaptation confirm
The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".
The flag is currently off.
|
| | |
| |
| |
| |
| |
| | |
With this commit, it is possible to write notations so that singleton
lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the
ability to remove notations from the parser.
|
| | | |
|
| | |
| |
| |
| | |
and global for 8.4 and 8.5.
|
| | | |
|
| |\ \ |
|
| |\ \ \
| | |/
| |/| |
|
| | | |
| | |
| | |
| | | |
there is actually no change in default subst between 8.4 and 8.5.
|
| |\| | |
|
| | |\ \
| | | |
| | | |
| | | | |
into v8.5
|
| |\| | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | | | |
|
| |\| | | |
|
| | | | | |
|
Jason Gross
Maxime Dénès
Théo Zimmermann
Gaëtan Gilbert
Pierre Letouzey
Hugo Herbelin
Pierre-Marie Pédrot
Guillaume Melquiond
Matej Kosik
Matthieu Sozeau
Paul Steckler
Jason Gross