| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | |
| |
| |
| |
| | |
definition, if they manipulate structures depending on the initial state
of the context.
|
| | |
| |
| |
| |
| | |
constr, and the associated signature, not needed anymore.
Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
- Introduced an error: fold was counting in the wrong direction and I
did not test it. Sorry.
- Substitution from params-with-let to params-without-let was still
not correct.
Hopefully everything ok now. Eventually, we should use canonical
combinators for that: extended_rel_context to built the instance and
and a combinator apparently yet to define for building a substitution
contracting the let-ins.
|
| | |
| |
| |
| | |
pattern-matching on function calls.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
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.
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
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.
|
Pierre-Marie Pédrot
Matthieu Sozeau
Hugo Herbelin
Maxime Dénès
Matthieu Sozeau
Jason Gross