| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Note that extracting terms containing primitive projections is still
utterly broken, so don't use them.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
|
| |
rejected.
|
| | |
|
| | |
|
| |
|
|
| |
Disclaimer: I have no idea what I am doing.
|
| |
|
|
| |
Also register properly the kind of definition.
|
| | |
|
| |
|
|
|
|
|
|
| |
When a notation was starting or ending a space, Coq assumed the notation
had no terminal symbol in either places. Coq also considered a notation
containing only spaces to be productive. As stated in the documentation,
extraneous spaces are only meant as printing hints, they are not meant to
have any influence on parsing.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
When encountering a "simpl nomatch" constant, the reduction machinery tries
to unfold it. If the subsequent partial reduction does not produce any
match construct, it keeps going from the reduced term. Unfortunately, the
reduced term has been refolded in the meantime, which means that some of
the previous reduction steps have been canceled, thus causing an infinite
loop. This patch delays the refolding till the very end, so that reduction
always progresses.
Disclaimer: I have no idea what I am doing here. The patch compiles the
standard library and the test suite properly, so hopefully they contain
enough tests to exercise the reduction machinery.
|
| |
|
|
|
|
|
|
|
|
|
| |
As noticed by Cyprien Mangin, projected terms cannot directly be used as
head values. Indeed, they might be applications (e.g. constructors as in
the bug report) whose arguments would thus be missing from the evaluation
stack when doing any iota-reduction step.
The only case where it would make sense is when the evaluation stack is
empty, as an optimization. Indeed, in that case, the arguments are put on
the stack, and then immediately put back inside the term.
|
| |
|
|
|
| |
constants up to their canonical name (taken from Daniel's
formalization of Puiseux theorem).
|
| | |
|
| |
|
|
|
| |
while eta-expanding a notation) + a more serious variant of it
(alpha-conversion incorrect wrt eta-expansion).
|
| |
|
|
|
|
|
|
|
|
|
| |
This is a follow-up on Matthieu's 7e7b5684
The Definition command was classified incorrectly when a body was provided.
This fix is a bit ad-hoc. A better one would require more expressiveness in
side effect classification, but I'll do it in trunk only since it could impact
plugins.
Thanks a lot to Enrico for his help!
|
| |
|
|
|
|
| |
Falling back to the global setting if not given.
Useful to make Add Morphism fail correctly when the given proof terms
are incomplete. Adapt test-suite file #2848 accordingly.
|
| |
|
|
|
| |
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.
|
| |
|
|
|
| |
As if we were adding : Type. Consistent with inductives with no
declared arity.
|
| | |
|
| | |
|
| |
|
|
| |
Forcefully equating it to the inferred level is not always desirable or possible.
|
| |
|
|
| |
So adding a test-suite file and closing the bug.
|
| |
|
|
|
|
|
|
|
| |
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).
|
| |
|
|
| |
They were not parsed correctly with a newline in the middle.
|
| |
|
|
| |
Add test-suite file to ensure non-regression.
|
| |
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
Checking that a term was indeed a relation was made too early, as the
decomposition function recognized relations of the form "f (g .. (h x y))
with f, g unary and only h binary. We postpone this check to the very end.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Print and Extraction commands may pierce opacity: if the
task producing the proof term is not finished, we wait for
its completion.
In -quick mode no worker is going to process a task, since tasks
are simply stored to disk (and resumed later in -vio2vo mode).
This commit avoids coqc waits forever for a task in order to
Print/Extract the corresponding term. Bug reported privately
by Alec Faithfull.
|
| |
|
|
|
| |
The setoid_rewrite tactic was not checking that the relation it was looking for
was indeed a relation, i.e. that its type was an arity.
|
| |
|
|
|
|
|
|
| |
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.
|
| | |
|
| |
|
|
|
|
| |
We simply handle the "break" in error messages. Not sure it is the
proper bugfix though, we may want to be able to add breaks in such
recursive notations.
|
| | |
|
| |
|
|
| |
variables and definitions in sections is unsupported.
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Function is_constructor was not properly fixed. Additionally, this fixes
a problem with the 8.5 interpretation of in-pattern (see Cases.v).
|
| |
|
|
|
| |
This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
|
| |
|
|
|
|
|
|
| |
evars were created making in turn that evars formerly recognized as
pending were not anymore in the list of pending evars). This also
fixes the reopening of #3848.
See comments on #4484 for details.
|
| |
|
|
| |
constant and arguments _separately_.
|
Pierre-Marie Pédrot
Hugo Herbelin
Guillaume Melquiond
Maxime Dénès
Matthieu Sozeau
Jason Gross
Matthieu Sozeau
Enrico Tassi