| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
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.
|
|
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).
|
|
|
|
|
|
|
|
|
|
|
