| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| |
| | |
constants up to their canonical name (taken from Daniel's
formalization of Puiseux theorem).
|
| | |
| |
| |
| | |
clause of a "match" over an irrefutable pattern.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
Thanks to Matthieu for the example.
|
| | |
| |
| |
| |
| | |
Passing `-compat 8.4` now allows the use of `econstructor (tac)`, as in
8.4.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
product in setoid_rewrite.
Before commit e8c47b652, it was raising an error which has been turned
to an anomaly.
This impacted Compcert where the former error was (apparently) caught
so that setoid_rewrite was returning back to ordinary rewrite.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| | |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
notations in patterns than in terms, wrt implicit arguments and
scopes.
See file Notations2.v for the conventions in use in terms.
Somehow this could be put in 8.5 since it puts in agreement the
interpretation of abbreviations and notations in "symmetric patterns"
to what is done in terms (even though the interpretation rules for
terms are a bit ad hoc).
There is one exception: in terms, "(foo args) args'" deactivates the
implicit arguments and scopes in args'. This is a bit complicated to
implement in patterns so the syntax is not supported (and anyway, this
convention is a bit questionable).
|
| | |
| |
| |
| |
| |
| | |
arguments and scopes with abbreviations and notations.
Comments are welcome on the proposed solutions for uniformization.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
E.g., Inductive foo := mkFoo { bla : foo } allowed to define recursive
records with eta for which conversion is incomplete.
- Eta-conversion only applies to BiFinite inductives
- Finiteness information is now checked by the kernel (the constructor types
must be strictly non recursive for BiFinite declarations).
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| | |
Try first to find a keyed subterm without conversion/betaiota on open
terms (that is the usual strategy of rewrite), if this fails, try with full
conversion, incuding betaiota. This makes the test-suite pass again,
retaining efficiency in the most common cases.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
in cctac which does not support indices properly.
Incidentally, this should fix a failure in RelationAlgebra, where
making prod_applist more robust (e8c47b652) revealed the discriminate
bug in congruence.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| | |
The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| | |
Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
|
| | |
| |
| |
| | |
constant and arguments _separately_.
|
| | | |
|
| | | |
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
Change was introduced by cedcfc9bc386456f3fdd225f739706e4f7a2902c.
|
| | | |
|
| |\| |
|
| | | |
|
| | | |
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
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.
|
| |\| |
|
| | |
| |
| |
| |
| |
| | |
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
| | | |
|
| |\| |
|
Pierre-Marie Pédrot
Hugo Herbelin
Jason Gross
Maxime Dénès
Matthieu Sozeau
Matthieu Sozeau
Enrico Tassi
Pierre Letouzey
Gregory Malecha