| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |\
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
| | |
| |
| |
| | |
Will be displayed on the website, but not part of the package.
|
| | | |
|
| |\ \
| | |
| | |
| | | |
into JasonGross-trunk-function_scope
|
| | | |
| | |
| | |
| | |
| | | |
Amongs other things, it kind of fixes bug #4492, even though you cannot really
take advantage of the parsed data for now.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Basically, the hypotheses were treated in an incorrect order, with a
hack for sometimes put them again in the right order, resulting in
failures and redundant hypotheses.
Status unclear, because this new version is incompatible except in
simple cases like a double induction on two "nat".
Fixing the bug incidentally simplify the code, relying on the
deprecation since 8.4 to allow not to ensure a compatibility (beyond
the simple situation of a double induction on simple datatypes).
See file induct.v for effect of changes.
|
| |\ \ \
| | |/
| |/| |
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The option is still there, but not documented since it is too
dangerous. Hints and type classes instances are not taking cleared
variables into account.
|
| |\| | |
|
| | | | |
|
| | | | |
|
| |\| | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
Marking it as experimental.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
based on a suggestion of Guillaume M. (done like this in ssreflect).
This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
|
| | | | |
|
| |\| | |
|
| | | | |
|
Hugo Herbelin
Matthieu Sozeau
Maxime Dénès
Matthieu Sozeau
Daniel de Rauglaudre
Jason Gross
Enrico Tassi
Pierre-Marie Pédrot
Guillaume Melquiond