| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
| |
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.
|
| |
|
|
|
| |
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 "_".
|
| |\ \ \ \ |
|
| | |/ / /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
|
Hugo Herbelin
Gaëtan Gilbert
Maxime Dénès
Jasper Hugunin
Théo Zimmermann
Pierre-Marie Pédrot
Paul Steckler
Matthieu Sozeau
Emilio Jesus Gallego Arias
Pierre Letouzey
Matthieu Sozeau
Gaëtan Gilbert