| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
With the "apply in" introduction pattern, and the backtrack possibly
done in "apply" over the components of conjunctions
(descend_in_conjunctions), the reasons for failing might have
different sources.
We give priority to the detection of used names over other
(unification) errors so that an error there is not masked in the
backtracking made by descend_in_conjunctions.
Of course, the question of what best unification error to give in the
presence of backtracking is still open.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- Fixing a typo introduced in 31dbba5f.
- Adapting to computation of universe constraints in pretyping.
- Adding a regression test.
|
|
|
|
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.
|
