| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| | |\
| | |
| | |
| | | |
Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
|
| | | |
| | |
| | |
| | | |
We also add a Coq86.v compat file.
|
| | | |
| | |
| | | |
This way, it's not eaten by a section
|
| | | |
| | |
| | | |
This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold <application of Facts>.option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | | |
Otherwise we may backtrack on the resolution in a
by which seems strange.
|
| | | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | | |
They were already commented out, Pierre confirms they're spurious.
|
| | | |
| | |
| | |
| | |
| | |
| | | |
Add a substitution of a local variable by its body to
ensure proper unification without having to make all local
variables unfoldable.
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
implicit is found whether one writes (sig P) or {x|P x}.
|
| | | |
| | |
| | |
| | | |
does not print to ** which is a keyword.
|
| | |/
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | | | | |
|
Hugo Herbelin
Pierre-Marie Pédrot
Maxime Dénès
Jason Gross
Jason Gross
Matthieu Sozeau
Pierre Letouzey