| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| |/ |
|
| |\
| |
| |
| | |
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.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Formerly, mk_refgoals in logic.ml was applying full βι on new Meta-based goals.
We simulate part of this βι-normalization in pose_all_metas_as_evars.
I suspect that we don't βι-normalize goals more than in 8.4 by doing
that, since all Metas would have eventually gone to mk_refgoals, but
difficult to know for sure as there were probably metas turned to
evars (and hence a priori not βι-normalized) even when logic.ml was
used more pervasively.
However, βι-normalizing is a priori a better heuristic than no
βι-normalizing, independently of what it was in 8.4 and before (even
if, ideally, I would personally lean towards preferring a
"chirurgical" substitution with reduction only at the place of
substitution).
|
| |\ \ \ |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | |/
| |/| |
|
| | | | |
|
| |/ / |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
This is probably the hardest case of them all, because tclABSTRACT fundamentally
relies on the names of universes from the constant instance being the same as
the one in the current goal. Adding to that the fact that the kernel is doing
strange things when provided with a polymorphic definition with body universe
constraints, it turns out to be a hellish nightmare to handle properly.
At some point we need to clarifiy this in the kernel as well, although we
leave it for some other patch.
|
| | | |
|
Anton Trunov
Maxime Dénès
Gaëtan Gilbert
Paul Steckler
Matthieu Sozeau
Hugo Herbelin
Théo Zimmermann
Emilio Jesus Gallego Arias
Pierre Letouzey
Matthieu Sozeau
Gaëtan Gilbert
Amin Timany
Pierre-Marie Pédrot