| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
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)
|
|
|
|
Everywhere we know that the universes of the left argument are an
extension of the right argument, we do not have to merge universes.
|
|
The clenv_fchain function was needlessly merging universes coming from
two evarmaps even though one was an extension of the other. A flag was
added so that the tactic just retrieves the newer universes.
|
|
about the prehistory of Coq.
|
|
Modules inserted into the environment were not hashconsed, leading to an
important redundancy, especially in module signatures that are always fully
expanded.
This patch divides by two the size and memory consumption of module-heavy
files by hashconsing modules before putting them in the environment. Note
that this is not a real hashconsing, in the sense that we only hashcons the
inner terms contained in the modules, that are only mapped over. Compilation
time should globally decrease, even though some files definining a lot of
modules may see their compilation time increase.
Some remaining overhead may persist, as for instance module inclusion is not
hashconsed.
|
|
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.
|
|
|
|
Mention compatibility file.
|
|
|
|
So as not to clutter the text. Also took the opportunity to add a few missing references.
|
|
|
|
Don't use abbreviated first names in sentences.
|
|
|
|
Formatting markup + typography.
|
|
|
|
unification (not necessarily preserved due to the fo approximation rule).
|
|
only one disjoint component of the typeclasses instances to resolve.
|
|
|
|
|
|
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] ..].
|
|
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.
|
