| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Error happened only when writing:
functional induction f x y z.
instead of
functional induction (f x y z).
Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
multiple pages.
Reviewed-by: jfehrle
|
|
implicit types
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
|
|
Ack-by: gares
Ack-by: ppedrot
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: cpitclaudel
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Reviewed-by: anton-trunov
Reviewed-by: ejgallego
|
|
Reviewed-by: MSoegtropIMC
|
|
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
runtime.
Reviewed-by: herbelin
|
|
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.
|
|
Closes #12232.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
|
|
See #11840 for a motivation. I had to fix Floats.FloatLemmas because
it uses the same name for a notation and a term, and the fact this
unfold was working on this was clearly a bug. I hope nobody relies
on this kind of stuff in the wild.
Fixes #5764: "Cannot coerce ..." should be a runtime error.
Fixes #5159: "Cannot coerce ..." should not be an error.
Fixes #4925: unfold gives error on Admitted.
|
|
|
|
We take the env of the current goal with the context replaced with
section variables. In practice, this is the global env, but, maybe,
one day, a goal state will have its own env.
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
