| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
|
Also fixing a bug of get_next_hyp_position when the hypothesis is the
oldest of the context (see test in ltac.v).
|
|
It allows in particular to have "Info" on tactic "assert" and
derivatives not to give an "<unknown>".
|
|
|
|
|
|
On some benchmarks provided by Chantal Keller a long time ago,
romega was abnormally slow compared to omega (or lia).
It turned out that the change of concl by reified version was
triggering unnecessary unfolds of Z.add, instead of unfolding
ReflOmegaCore.Z_as_Int.plus into Z.add. This is now fixed by
the various Parameter Inline : no more indirections, Z_as_Int.plus
is directly Z.add.
Also use Tactics.convert_concl_no_check for this "change", as
recommended by PMP.
|
|
|
|
Due to some unknown problem coqchk fails on some inductive types when it is
compiled with ocaml4.02.3+32bit and camlp5-4.16 which is the case for Travis
tests.
|
|
Fix a mistake in record declaration
|
|
|
|
|
|
|
|
|
|
The user now has to manually load them, respectively via:
Require Extraction
Require Import FunInd
The "Import" in the case of FunInd is to ensure that the
tactics functional induction and functional inversion are indeed
in scope.
Note that the Recdef.v file is still there as well (it contains
complements used when doing Function with measures), and it also
triggers a load of FunInd.v.
This change is correctly documented in the refman, and the test-suite
has been adapted.
|
|
|
|
|
|
|
|
See now https://github.com/coq/bignums
Int31 is still in the stdlib.
Some proofs there has be adapted to avoid the need for BigNumPrelude.
|
|
Also taking into account a name in the return clause and in the
indices.
Note the double meaning ``bound as a term to match'' and ``binding in
the "as" clause'' when the term to match is a variable for all of
"match", "if" and "let".
|
|
|
|
short econstr-cleaning of record.ml
|
