| Age | Commit message (Collapse) | Author |
|---|
|
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] ..].
|
|
introduction pattern by default.
|
|
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.
|
|
changes from final 8.5 to next version.
|
|
for more regularity.
|
|
Did some manual merge in tactics/tactics.ml.
|
|
|
|
|
|
For instance,
Inductive a (x:=1) := C : a -> True.
was wrongly reporting
Error: The type of constructor C
is not valid; its conclusion must be
"a" applied to its parameter.
Also "simplifying" explain_ind_err.
|
|
|
|
|
|
|
|
printing the type of the defined term of a LetIn).
|
|
|
|
which e.g. OCaml 4.02.1 displays.
|
|
Hopefully, it will provide with nicer proof terms, in combination with
the commit printing the type of LetIn when the defined term is a proof.
|
|
this type is a proposition. This is based on the assumption that in
Prop, what matters first is the statement.
|
|
|
|
For pose/set/clearbody, I think it is clear that we want to preserve
the name and this commit do it.
For revert, I first did not preserve the name, then considered in
2ba2ca96be88 that it was better to preserve it.
For intro, like for revert actually, I did not preserve the name,
based on the idea that the type was changing (*). For instance if we have
?f:nat->nat, do we really want to keep the name f in ?f:nat after an
intro.
For revert, I changed my mind based on the idea that if we had a
better control of the name if we keep the name that if the system
invents a new one based on the type. I think this is more reasonable
than (*), so this commit preserves the name for intro.
For generalize, it is still not done because of generalize being in
the old proof engine.
|
|
|
|
|
|
- Had to add a Sigma.to_evar_map
- Had to rework coqdep_common.ml{,i} and coqdep.ml
|
|
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
|
|
|
|
|
|
|
|
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.
|
|
|
|
Syntactic analysis of dependencies when atomizing arguments in destruct
was not dealing properly with primitive projections hiding their
parameters.
|
|
|
|
|
|
proofs.
|
|
whd_evar in refresh_universes.
|
|
|
|
inconsistent).
|
|
When refreshing a type variable, always use a rigid universe to force the most
general universe constraint, as in 8.4.
|
|
is buggy in general.
|
|
|
|
Now doing
```coq
Tactic Notation "left" "~" := left.
Tactic Notation "left" "*" := left.
```
will no longer break the `left` tactic in Coq 8.4.
List obtained via
```
grep -o '^ \[[^]]*\]' tactics/coretactics.ml4 | sed s'/^ \[ \(.*\) \]/Tactic Notation \1 := \1./g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\)"/\1/g' | sed s'/\(:=.*\) \(constr\|bindings\|constr_with_bindings\|quantified_hypothesis\|ne_hyp_list\)(\([^)]*\))/\1 \3/g'
```
|
|
|
|
|
|
make them rigid to disallow minimization.
|
|
|
|
|
|
its main interest!
|
|
The "master" label used to be reset to the wrong id
|
|
|
|
|
|
When a future is fully forced (joined), the fix_exn is dropped,
since joined futures are values (hence they cannot raise exceptions).
When a future for a transparent definition enters the environment
it is joined. If one needs to pick its fix_exn, he should do it
before that.
|
