| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
| |
| |
| | |
This reverts commit dbe29599c2e9bf49368c7a92fe00259aa9cbbe15.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Notation "## c" := (S c) (at level 0, c at level 100).
which break the stratification of precedences. This works for the case
of infix or suffix operators which occur in only one grammar rule,
such as +, *, etc. This solves the "constr" part of #3709, even though
this example is artificial.
The fix is not complete. It puts extra parenthesese even when it is
end of sentence, as in
Notation "# c % d" := (c+d) (at level 3).
Check fun x => # ## x % ## (x * 2).
(* fun x : nat => # ## x % (## x * 2) *)
The fix could be improved by not always using 100 for the printing
level of "## c", but 100 only when not the end of the sentence.
The fix does not solve the general problem with symbols occurring in
more than one rule, as e.g. in:
Notation "# c % d" := (c+d) (at level 1).
Notation "## c" := (S c) (at level 0, c at level 5).
Check fun x => # ## x % 0.
(* Parentheses are necessary only if "0 % 0" is also parsable *)
I don't see in this case what better approach to follow than
restarting the parser to check reversibility of the printing.
|
| | |
| |
| |
| | |
clause of a "match" over an irrefutable pattern.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| | |
with a more explicit message.
|
| | |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| | |
Thanks to Matthieu for the example.
|
| | |
| |
| |
| |
| | |
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.
|
| |\ \
| | |
| | |
| | | |
into JasonGross-trunk-function_scope
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| |\ \ \
| | |/
| |/| |
|
| | | | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | |
| | |
| | |
| | | |
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.
|
| |\| | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
This gets rid of brittle code written in ML files through Ltac quotations, and
reduces the dependance of Coq to such a feature. This also fixes the particular
instance of bug #2800, although the underlying issue is still there.
|
| |\| | |
|
| | | | |
|
Guillaume Melquiond
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Jason Gross
Matthieu Sozeau