| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Marking it as experimental.
|
|
|
|
|
|
|
|
|
|
based on a suggestion of Guillaume M. (done like this in ssreflect).
This is actually consistent with the hack of using "destruct (1)" to
mean the term 1 by opposition to the use of "destruct 1" to mean the
first non-dependent hypothesis of the goal.
|
|
Do not substitute rigid variables during minimization, keeping
their equality constraints instead.
|
|
|
|
|
|
pat/c1/.../cn behaves as intro H; apply c1, ... , cn in H as pat.
Open to other suggestions of syntax though.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Prop levels.
As they are typed assuming all variables are >= Set now, and this was
breaking an invariant in typing. Only one instance in the standard
library was used in Hurkens, which can be avoided easily. This also
avoids displaying unnecessary >= Set constraints everywhere.
|
|
The fix was actually elementary. The lexer comes with a function to
compare parsed tokens against tokens of the parsing rules. It is
enough to have this function considering an ident in a parsing rule to
be equal to the corresponding string parsed as a keyword.
|
|
|
|
parameters of an inductive type.
|
|
|
|
Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in
8.5beta2 and 8.5beta3 from a Coq file because typing done while
compiling "match" would serve as a protection. However exploitable by
calling the kernel directly, e.g. from a plugin (but a plugin can
anyway do what it wants by bypassing kernel type abstraction).
Fixing similar error in pretyping.
|
|
|
|
The issue was due to the fact that unfold hints are given a priority of 4
by default. As eauto was now using hint priority rather than the number of
goals produced to order the application of hints, unfold were almost always
used too late. We fixed this by manually giving them a priority of 1 in the
eauto tactic.
Also fixed the relative order of proof depth w.r.t. hint priority. It should not
be observable except for breadth-first search, which is seldom used.
|
|
projections.
- lift accounting for the record missing in computing the subst from
fields to projections of the record
- substitution for parameters should not lift the local definitions
- typo in building the latter (subst -> letsubst)
|
|
Not sure if this is really what is expected though.
|
|
|
|
We retypecheck the hypotheses introduced by the refine primitive instead of
blindly trusting them when the unsafe flag is set to false.
|
|
|
|
|
|
|
|
their type annotation.
|
|
We just handle unnamed implicits using a dummy name. Note that the implicit
argument logic should still output warnings whenever the user writes implicit
arguments that won't be taken into account, but I'll leave that for another
time.
|
|
default. Interestingly, there is an example where it makes the rest of
the proof less natural.
Goal forall x y:Z, ...
intros [y|p1[|p2|p2]|p1[|p2|p2]].
where case analysis on y is not only in the 2nd and 3rd case, is not
anymore easy to do.
Still, I find the bracketing of intro-patterns a natural property, and
its generalization in all situations a natural expectation for
uniformity. So, what to do? The following is e.g. not as compact and
"one-shot":
intros [|p1|p1]; [intros y|intros [|p2|p2] ..].
|
|
This reverts commit 07620386b3c1b535ee7e43306a6345f015a318f0.
Very sorry not ready.
|
|
the return clause and of the branches in a "match", computing them
automatically when using the "at" clause of pattern, destruct, ...
In principle, this is a source of incompatibilities in the numbering,
since the internal binders of a "match" are now skipped. We shall deal
with that later on.
|
|
Did some manual merge in tactics/tactics.ml.
|
|
|
|
printing the type of the defined term of a LetIn).
|
|
|
|
|
|
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
|
|
|
for reporting it.
A "cut" was not appropriately chained on the second goal but on both
goals, with the chaining on the first goal introducing noise.
|
|
|
|
|
|
whd_evar in refresh_universes.
|
|
inconsistent).
|
