| Age | Commit message (Collapse) | Author |
|---|
|
|
|
When there is more than one variable to declare we stop trying to
attach global universes (ie monomorphic or section polymorphic) to one
of them.
|
|
|
|
Following up on #6791, we remove:
- `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes`
- `Match Strict` a deprecated NOOP.
|
|
|
|
|
|
|
|
|
|
size.
|
|
|
|
This test was actually checking that evar-containing terms were making the
VM fail. Obviously this is not the case anymore, so the test is now invalid.
|
|
|
|
Following up on #6791, we remove the option "Standard Proposition Elimination"
|
|
|
|
|
|
Fix new deprecation warnings in the standard library.
|
|
|
|
Noticed by Sigurd Schneider.
|
|
We test the 3 possible scenarios. A more complete test would also
involved fake_ide.
c.f. #6793
|
|
|
|
infinite eta-expansion)
|
|
|
|
As per https://github.com/coq/coq/pull/6756/files#r168028764
|
|
|
|
|
|
More precisely when matching
"f t" with "(fun ?x => .. ((fun ?x' => ?y) ?z') ..) ?z"
do not allow expansion of f since otherwise, we recursively have to
match "f t" with the same pattern.
|
|
Also changed the API of pr_subgoals now using labels.
Also removed a trailing space in printing existentials.
|
|
|
|
|
|
the concl
|
|
|
|
There is more churn than there should be because SearchPattern uses a
non-local sorting algorithm; the comparison function considers many
constants equal in priority and leaves it up to the heap structure to
break ties, which seems wrong. This has been reported as
[bug #5573](https://coq.inria.fr/bugs/show_bug.cgi?id=5573).
|
|
Computation of the sort of the inductive type was done before ensuring
that the arguments of the inductive type had the correct types,
possibly brutally failing with `NotArity` in case one of the types
expected to be typed with an arity was not so.
|
|
|
|
Concretely, we bypass the following limitation: The notation
"{ ' pat | P }" broke the parsing of expressions of the form
"{ forall x, P } + { Q }". Indeed the latter works thanks to a
tolerance of Camlp5 in parsing "forall x, P" at level 200 while the
rule asks to actually parse the interior of "{ ... }" at level 99 (the
reason for 99 is to be below the rule for "M : T" which is at level
100, so that "{ x : A | P }" does not see "x : A" as a cast). Adding
an extra "'"; pat = pattern in parallel to c = constr LEVEL "99" broke
the tolerance for constr at level 200.
We fix this by adding an ad hoc rule for "{ binder_constr }" in the
native grammar (g_constr.ml4).
Actually, this is inconsistent with having a rule for "{ constr at level 99 }"
in Notations.v. We should have both rules in Notations.v or both rules
hard-wired in the native grammar. But I still don't know what is the best
decision to take, so leaving as it at the current time.
Advantages of hard-wiring both rules in g_constr.ml4: a bit simpler in
metasyntax.ml (no need to ensure that the rule exist). Disadvantages:
if one wants a different initial state without the business needing
the "{ }" for sumbool, sumor, sig, sigT, one still have the rules
there.
Advantages of having them in Notations.v: more modular, we can change
the initial state. Disadvantages: one would need a new kind of
modifier, something like "x at level 99 || binder_constr", with all
the difficulty to find a nice, intuitive, name for "binder_constr",
and the difficulty of understanding if there is a generality to this
"||" disjunction operator, and whether it should be documented or not.
|
|
|
|
For compatibility, the default is to parse as ident and not as pattern.
|
|
Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".
This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.
The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.
|
|
We reason up to order, and accept to match a final catch-all clauses
with any other clause.
This allows for instance to parse and print a notation of the form
"if t is S n then p else q".
|
|
This now works not only for parsing of fun/forall (as in 8.6), but
also for arbitraty notations with binders and for printing.
|
|
Example which is now reprinted as parsed:
fun '((x,y) as z) => (y,x)=z
|
|
To deal with existing notations starting with a "let" (see notation
"for" in output/Notation2.v) we adopt the pragmatic approach of
glueing only inner let by default.
Ideally, it might be nicer to detect if there is an overlap of
notation, and not to glue only in case of overlap. We could also
decide that a notation starting with a "let" should always be
protected by some constant, say "id", so as to avoid possible
collisions, but this would require changes user side.
|
|
For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.
We let the general case absorb this particular case.
We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).
Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?
|
|
|
|
This allows in particular to define notations with 'pat style binders.
E.g.:
A non-trivial change in this commit is storing binders and patterns
separately from terms.
This is not strictly necessary but has some advantages.
However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).
So, it is as simple to always store idents (and eventually patterns)
as terms.
|
|
For instance, the following is now possible:
Check {(x,y)|x+y=0}.
Some questions remains. Maybe, by consistency, the notation should be
"{'(x,y)|x+y=0}"...
|
|
|
|
Seizing this opportunity to generalize the possibility for different
associativity into simply reversing the order or not. Also dropping
some dead code.
Example of recursive notation now working:
Notation "[ a , .. , b |- A ]" := (cons b .. (cons a nil) .., A).
|
|
This allows for instance to support recursive notations of the form:
Notation "! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
|
|
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
|
