| Commit message (Collapse) | Author | Age |
|---|
| ... | |
| | | | | | | | | |
|
| | | |_|_|/ / /
| |/| | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | |
| | | | | | | |
Since 260965d, an imperative code was semantically the identity because the
closure allocation was not performed at the right moment. Because of it
intricacy, I cannot really tell the original motivations of this piece of
code, although it looks like it was for there for pretty-printing of errors.
Anyway, both because the code was dubious and its effect not observed, it
cannot hurt to remove it.
|
| | | |/ / / /
| |/| | | |
| | | | | |
| | | | | | |
A universe substitution was lacking as the normalized evar map was dropped.
|
| | | |/ / /
| |/| | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
The code was assuming that the terms t and u for which {t=u}+{t<>u} is
proved were distinct. We refine an internal "generalize" of "u" so
that it works on the two precise occurrences to abstract, even if
other occurrences of u occur as subterm of t too.
We also reuse the global constants found in the statement rather than
reconstructing them (this seems better in case the global constants
eventually get polymorphic universes?).
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
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
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | | | | | |
|
| | | |/ / /
| |/| | | |
|
| | | | | |
| | | | |
| | | | |
| | | | | |
https://github.com/coq/coq/pull/201#discussion_r110957570
|
| | | | | |
| | | | |
| | | | |
| | | | | |
https://github.com/coq/coq/pull/201#discussion_r110952601
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
Also move named arguments to the beginning of the functions. As per
https://github.com/coq/coq/pull/201#discussion_r110928302
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This will allow a cache_term tactic that doesn't suffer from the
Not_found anomalies of abstract in typeclass resolution.
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This is a small change that allows a transparent version of tclABSTRACT.
Additionally, it factors the machinery of [abstract] through a
plugin-accessible function which allows alternate continuations (other
than exact_no_check.
It might be nice to factor it further, into a cache_term function that
caches a term, and a separate bit that calls cache_term with the result
of running the tactic.
|
| | | | | | |
|
| | | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | | |
This completes the Loc.ghost removal, the idea is to gear the API
towards optional, but uniform, location handling.
We don't print <unknown> anymore in the case there is no location.
This is what the test suite expects.
The old printing logic for located items was a bit inconsistent as
it sometimes printed <unknown> and other times it printed nothing as
the caller checked for `is_ghost` upstream.
|
| | | | | |
| | | | |
| | | | |
| | | | | |
Now it is a private field, locations are optional.
|
| | |_|/ /
|/| | | |
|
| | | | | |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
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.
|
Théo Zimmermann
Pierre-Marie Pédrot
Hugo Herbelin
Maxime Dénès
Gaetan Gilbert
Jason Gross
Emilio Jesus Gallego Arias