| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
|
|
|
| |
~True.
Found 1 incompatibility in tested contribs and 3 times the same
pattern of incompatibility in the standard library. In all cases, it
is an improvement in the form of the script.
New behavior deactivated when version is <= 8.5.
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| | |
Option Standard Proposition Elimination Scheme from 8.5 was not
documented in the right section.
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
Modulo delta for types should be fully transparent.
|
| |\| |
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| | |
A couple of bugs have been found.
Example #4932 is now printing correctly in the presence of multiple
binders (when no let-in, no irrefutable patterns).
|
| |\| |
|
| | |
| |
| |
| | |
We should really automate the generation of the log of fixes for CHANGES.
|
| |\| |
|
| | |
| |
| |
| | |
This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
|
| |\| |
|
| | |
| |
| |
| | |
not in pl2.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| |\ \
| | |
| | |
| | | |
Was PR#207: Add -no-print-dependent-evars
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Cf CHANGES for details.
|
| |/ /
| |
| |
| |
| | |
This allows a work-around for bug #4819,
https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
As noticed by C. Cohen it was confusingly different from standard
notation.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
computing the arguments which allows to decide which list of implicit
arguments to consider when several such lists are available.
For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _",
the same way as if we had said:
Arguments eq_refl {A} {x}.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
What one needs to know in 3rd party makefiles, like plugins ones,
is the Coq version and the OCaml version number. This option prints
the 2 values on a single line separated by spaces. The already existing
--version outputs the same piece of info but in a format meant for user
consumption, and hence harder to parse.
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
Add -o option to coqc
|
| |\ \ \ \
| |_|/ /
|/| | /
| | |/
| |/| |
|
| | | | |
|
| | |/
|/|
| |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
preserved, which is a source of incompatibilities w.r.t. released 8.5
but which looks to me to be the only possible canonical behavior.
This is I believe a better behavior than the Regular Subst Tactic
behavior in the released 8.5 and 8.5pl1. There, the order of
hypotheses in which substitutions happened was respected, but their
interleaving with other hypotheses was not respected.
So, I consider this to be a fix to the "Regular Subst Tactic" mode.
Also added a more detailed "specification" of the "Regular" behavior
of "subst" in the reference manual.
|
| |\| |
|
| | | |
|
| | | |
|
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Pierre-Marie Pédrot
Matthieu Sozeau
Daniel de Rauglaudre
Jason Gross
Enrico Tassi