| Commit message (Collapse) | Author | Age |
|---|
| |\ |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
|
| | |
| |
| |
| | |
A priori considered to be a good programming style.
|
| |\ \
| | |
| | |
| | | |
let-ins
|
| | | | |
|
| | | | |
|
| | | | |
|
| | | | |
|
| | |/
|/| |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The current implementation was still using continuation passing-style, and
furthermore was triggering a focus on the goals. We take advantage of the
tactic features instead.
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
The only remaining use was applied on the unfold tactic, and the behaviours
of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced
by their argument tactic.
|
| | |
| |
| |
| | |
The only use in Equality is reimplemented in the new engine.
|
| | |
| |
| |
| |
| |
| |
| |
| |
| | |
Today, both modes are controlled by a single flag, however this is a
bit misleading as is_silent really means "quiet", that is to say `coqc
-q` whereas "verbose" is Coq normal operation.
We also restore proper behavior of goal printing in coqtop on quiet
mode, thanks to @Matafou for the report.
|
| | |
| |
| |
| |
| |
| |
| |
| | |
- Supporting let-ins in tactic "fix", and hence in interactive
Fixpoint and mutual theorems.
- Documenting more precisely the meaning of n in tactic "fix id n".
- Fixing computation of recursive index at interpretation time in the
presence of let-ins.
|
| | |
| |
| |
| |
| |
| | |
The evarmap used by the heuristic could contain resolved evars, which could
lead to a failure of backtracking in the EConstr branch. This is experimental
and may be to costly.
|
| |\| |
|
| | |\ |
|
| | | |
| | |
| | |
| | |
| | |
| | | |
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
|
| | | |
| | |
| | |
| | |
| | | |
For now we only normalize sorts, and we leave instances for the next
commit.
|
| |\| | |
|
| | |\ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We make apparent in the API that the implicit tactic is set or not. This was
costing a lot in Pretyping for no useful reason, as it is almost always unset
and the default implementation was just failing immediately.
|
| | | |/
| |/|
| | |
| | |
| | |
| | | |
All functions where actually called with the second argument of the pending
problem being the current evar map. We simply remove this useless and
error-prone second component.
|
| | | |\ |
|
| | |\| | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
- Adding a better location in the "apply" on the fly pattern.
- Printing statement of lemma and of hypothesis.
Was suggested by discussion at wish report #5390.
|
| | | | |
| | | |
| | | |
| | | | |
This warning was shown in CoqIDE but not by coqc.
|
| | | |\ \
| | | |/
| | |/|
| | | | |
correctly as…
|
| |\| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Interpretation of patterns in Ltac is essentially flawed. It does a roundtrip
through the pretyper, and relies on suspicious flagging of evars in the evar source
field to recognize original pattern holes. After the pattern_of_constr function
was made evar-insensitive, it expanded evars that were solved by magical side-effects
of the pretyper, even if it hadn't been asked to perform any heuristics.
We backtrack on the insensitivity of the pattern_of_constr function. This may have
a performance penalty in other dubious code, e.g. hints. In the long run we should
get rid of the pattern_of_constr function.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The underlying hint mode implementation was not using the evar-insensitive
API so that it resulted in strange bugs.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
Now they are useless because all of the primitives are (should?) be
evar-insensitive.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This is now useless as this returns evar-constrs, so that all functions acting
on them should be insensitive to evar-normalization.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We make mli files look to what they were looking before the move to EConstr
by opening this module.
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
| | | | | |
|
Maxime Dénès
Théo Zimmermann
Hugo Herbelin
Gaetan Gilbert
Pierre-Marie Pédrot
Emilio Jesus Gallego Arias