| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
patterns.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
They were deprecated in 8.12.
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
All calls to this function are now factorized through Clenvtac.res_pf.
|
|
|
|
Fixes #12571.
|
|
Instead of dropping the unification result and calling simple eapply with
the original term, we simply use the same code path as auto and typeclass
eauto, i.e. reuse the clenv for refinement.
|
|
Reviewed-by: herbelin
|
|
It is only used for this kind of hints, never for Extern / Unfold.
|
|
|
|
The only use was seemingly a bug introduced in 0aec9033a by an accidental
variable capture. There is indeed no reason that the set of variables of a
hint corresponds to the one of the current environment.
|
|
|
|
|
|
|
|
They are always the same.
|
|
There is no point in warning about eauto being the only one able to use those
hints, since they will be used by typeclass_eauto instead. It was probably an
oversight introduced quite a long time ago.
|
|
They were always instantiated with the triple (true, false, false).
|
|
|
|
This is barely more meaningful but at least we do not rely on an antiquated
API now.
|
|
|
|
|
|
|
|
Reviewed-by: herbelin
|
|
|
|
|
|
|
|
No need to create various mapping of lists when a filter would suffice.
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
It was deprecated in 8.12 and not used in the wild.
|
|
|
|
This allows to remove internal API from the mli as well.
|
|
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict
match to an hypothesis or the conclusion, possibly only at the head
(like SearchHead in this latter case)
- new clause "is:" to search by kind of object (for some list of kinds)
- support for any combination of negations, disjunctions and conjunctions,
using a syntax close to that of intropatterns.
|
|
Current backtraces for tactics leave a bit to desire, for example
given the program:
```coq
Lemma u n : n + 0 = n.
rewrite plus_O_n.
```
the backtrace stops at:
```
Found no subterm matching "0 + ?M160" in the current goal.
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
Backtrace information `?info` is as of today optional in some tactics,
such as `tclZERO`, it doesn't cost a lot however to reify backtrace
information indeed in `tclZERO` and provide backtraces for all tactic
errors. The cost should be small if we are not in debug mode.
The backtrace for the failed rewrite is now:
```
Found no subterm matching "0 + ?M160" in the current goal.
Raised at file "pretyping/unification.ml", line 1827, characters 14-73
Called from file "pretyping/unification.ml", line 1929, characters 17-53
Called from file "pretyping/unification.ml", line 1948, characters 22-72
Called from file "pretyping/unification.ml", line 2020, characters 14-56
Re-raised at file "pretyping/unification.ml", line 2021, characters 66-73
Called from file "proofs/clenv.ml", line 254, characters 12-58
Called from file "proofs/clenvtac.ml", line 95, characters 16-53
Called from file "engine/proofview.ml", line 1110, characters 40-46
Called from file "engine/proofview.ml", line 1115, characters 10-34
Re-raised at file "clib/exninfo.ml", line 82, characters 4-38
Called from file "proofs/proof.ml", line 381, characters 4-42
Called from file "tactics/pfedit.ml", line 102, characters 31-58
Called from file "plugins/ltac/g_ltac.mlg", line 378, characters 8-84
```
which IMO is much better.
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
indirectly dependent in goal
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
|
|
