| Age | Commit message (Collapse) | Author |
|---|
|
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
|
|
of standard infrastructure.
Reviewed-by: ppedrot
|
|
Apart from being verboten to marshal Environ.env, this should use much less
memory on-disk.
Fixes #12707.
|
|
infrastructure.
The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695
|
|
|
|
|
|
|
|
|
|
|
|
but ssrsearch is not loaded.
Fixes #12338
|
|
|
|
- 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
|
|
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.
|
|
multiple scopes for the same inductive)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
|
|
Moving code around uncovered this bug.
|
|
This function was used almost everywhere with the wrapper around.
|
|
same inductive)
Numeral Notations now play better with multiple scopes for the same
inductive. Previously, when multiple numeral notations where defined
for the same inductive, only the last one was considered for
printing. Now, we proceed as follows
1. keep only uninterpreters that produce an output (first
List.map_filter)
2. keep only uninterpretation for scopes that either have a scope
delimiter or are open (second List.map_filter)
3. the final selection is made according to the order of open scopes,
(find_uninterpretation) or or according to the last defined
notation if no appropriate scope is open (head of list at the end)
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
