| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | |
| | | |
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.
|
| | | |
|
| | | |
|
| |/
|
|
|
|
| |
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
| |
|
|
|
|
|
|
|
|
| |
This addresses a limitation found in math-comp seq.v file. See the example in
test suite file success/Notations2.v.
To go further and accept recursive notations with a separator made of
several tokens, and assuming camlp5 unchanged, one would need to
declare an auxiliary entry for this sequence of tokens and use it as
an "atomic" (non-terminal) separator. See PR #6167 for details.
|
| |\
| |
| |
| | |
(clause "where" with implicit arguments)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We improve one step further the heuristics to sort out if a variable
is a notation variable or a named variable.
This allows to support the following which was still failing.
Reserved Notation "# x" (at level 0).
Inductive I {A:Type} := C : # 0 -> I where "# I" := (I = I).
We rely here on the property that a binding variable of same name as a
notation variables is itself considered bound by the notation.
This becomes however to be a bit tricky for sorting out if the
variable has to be output to the glob file or not.
|
| |\ \
| |/
|/| |
|
| |\ \ |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | | |
Compared to the original proposition (59a594b in #960), this commit
only changes files containing bug numbers that are also PR numbers.
|
| |\ \ \ |
|
| | |/ /
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
The manual has long stated that these forms are deprecated. We add a
warning for them, as indeed `Add Morphism` is an "proof evil" [*]
command, and we may want to remove it in the future.
We've also fixed the stdlib not to emit the warning.
[*] https://ncatlab.org/nlab/show/principle+of+equivalence
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When a context variable x is of the form "x := body : Z",
romega is now made aware of this body. Technically, we reify an equation
x = body, and push a corresponding (eq_refl x) as argument of the
final do_omega.
See also the previous commit adding this same feature to omega
(fixing bug 142).
|
| |\ \
| | |
| | |
| | | |
cleared context.
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
| |/ /
| |
| |
| |
| |
| | |
The function Proofview.undefined was collecting twice the evars that
had advanced. Consequently, the functions Proofview.unshelve and
Proofview.with_shelf were possibly doing the same.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | | |
The bug was caused by an inconsistency in different part of the code
for deciding where cutting the context in between recursively uniform
parameters and non-recursively uniform ones when let-ins were in the
middle. We fix it by using uniformly "context_chop".
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
| |\ \ \
| |/ /
|/| | |
|
| | | | |
|
| |\ \ \
| | | |
| | | |
| | | | |
work better on them
|
| | | | |
| | | |
| | | |
| | | | |
For instance, we don't want "id@{u}" to be coerced to id, or "?[n]" to "_".
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
Hugo Herbelin
Jasper Hugunin
Gaëtan Gilbert
Maxime Dénès
Théo Zimmermann
Pierre-Marie Pédrot
Anton Trunov
Paul Steckler
Matthieu Sozeau
Emilio Jesus Gallego Arias
Pierre Letouzey
Matthieu Sozeau
Gaëtan Gilbert