| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
|
|
| |
We expected `nparams + nrealargs + consnrealargs` but the `nrealargs`
should not be there. This breaks cumulativity of constructors for any
inductive with indices (so records still work, explaining why the test
case in #6747 works).
|
| |\ |
|
| | |
| |
| |
| |
| |
| | |
In Reductionops.infer_conv we did not have enough information to
properly try to unify irrelevant universes. This requires changing the
Reduction.universe_compare type a bit.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Previously [fun x : Ind@{i} => x : Ind@{j}] with Ind some cumulative
inductive would try to generate a constraint [i = j] and use
cumulativity only if this resulted in an inconsistency. This is
confusingly different from the behaviour with [Type] and means
cumulativity can only be used to lift between universes related by
strict inequalities. (This isn't a kernel restriction so there might
be some workaround to send the kernel the right constraints, but
not in a nice way.)
See modified test for more details of what is now possible.
Technical notes:
When universe constraints were inferred by comparing the shape of
terms without reduction, cumulativity was not used and so too-strict
equality constraints were generated. Then in order to use cumulativity
we had to make this comparison fail to fall back to full conversion.
When unifiying 2 instances of a cumulative inductive type, if there
are any Irrelevant universes we try to unify them if they are
flexible.
|
| | | |
|
| |/ |
|
| |\ |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
wish #4129)
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Attempt to extract the current ongoing proof (request by
Clément Pit-Claudel on coqdev, and also #4129).
Evars are handled as axioms.
|
| | | | |
| | | |
| | | |
| | | | |
Following up on #6791, we the option "Shrink Abstract".
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
a record.
|
| |\ \ \ \ \ |
|
| |\ \ \ \ \ \ |
|
| |\ \ \ \ \ \ \ |
|
| | | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | |
| | | | | | | | |
Following up on #6791, we remove:
- `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes`
- `Match Strict` a deprecated NOOP.
|
| | | |/ / / / / |
|
| |\ \ \ \ \ \ \
| |_|/ / / / /
|/| | | | | | |
|
| | | |_|_|/ /
| |/| | | | |
|
| |/ / / / /
| | | | |
| | | | |
| | | | | |
Noticed by Sigurd Schneider.
|
| |/ / / / |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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}.
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
No using a mutable counter to skip them, instead we keep them in the
environment.
|
| |/ /
| |
| |
| | |
Was raised by Jason on Gitter.
|
| | |
| |
| |
| |
| | |
This ensures by construction that we never infer constraints outside
the variance model.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
Since cumulativity of an inductive type is the universe constraints
which make a term convertible with its universe-renamed copy, the only
constraints we can get are between a universe and its copy.
As such we do not need to be able to represent arbitrary constraints
between universes and copied universes in a double-sized ucontext,
instead we can just keep around an array describing whether a bound
universe is covariant, invariant or irrelevant (CIC has no
contravariant conversion rule).
Printing is fairly obtuse and should be improved: when we print the
CumulativityInfo we add marks to the universes of the instance: = for
invariant, + for covariant and * for irrelevant. ie
Record Foo@{i j k} := { foo : Type@{i} -> Type@{j} }.
Print Foo.
gives
Cumulative Record Foo : Type@{max(i+1, j+1)} := Build_Foo
{ foo : Type@{i} -> Type@{j} }
(* =i +j *k |= *)
|
| |\ \ |
|
| | | | |
|
| |\ \ \
| |/ /
|/| | |
|
| | | | |
|
| | | | |
|
| |/ /
| |
| |
| |
| |
| |
| | |
The main contender was the abstract tactic that was generating useless
constraints for polymorphic subproofs that happened to contain themselves
monomorphic subproofs. We had to fix the test-suite for one particular
corner-case instance that looked more like a bug than anything else.
|
| |/ |
|
| |\
| |
| |
| | |
Extraction Language command
|
| | | |
|
| |/ |
|
| | |
|
| |\
| |
| |
| | |
instance.
|
| |\ \
| | |
| | |
| | | |
of levels
|
| | |/
|/| |
|
| | |
| |
| |
| |
| |
| | |
Apparently a long-standing bug, coupled with a pattern/constr
associativity inconsistency introduced while fixing another
pattern/constr level inconsistency (bug #4272, 0917ce7c).
|
| | | |
|
| | |
| |
| |
| | |
Also nicer error when the constraints are impossible.
|
| | | |
|
| | | |
|
Jasper Hugunin
Gaëtan Gilbert
Maxime Dénès
charguer
Matthieu Sozeau
Pierre Letouzey
Emilio Jesus Gallego Arias
Théo Zimmermann
Pierre-Marie Pédrot
Hugo Herbelin
Anton Trunov
Paul Steckler
Matthieu Sozeau