| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | |
| |
| |
| | |
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.
|
| |\| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| |\| |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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).
|
| | |
| |
| |
| |
| | |
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_.
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| | |
Also ensure we stay compatible with 8.4: progress could now be made
simply because of beta redexes in the goal.
|
| |\| |
|
| | | |
|
| | |
| |
| |
| |
| | |
The side-effects can contain universe declarations needed to typecheck
later proofs, which weren't added to the env used to typecheck them.
|
| |\| |
|
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Enrico Tassi
Guillaume Melquiond