| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
|
|
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.
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
This is already protected by then enter block.
|
|
The inner body was not raising any exception since it was in the monad,
and even if it did so, the enter block would have caught it.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
|
|
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.
|
|
Since we don't always have the call trace anymore, we explicitly
insert a catch of failures in TacAlias. The trace is then treated in
this catch rather than propagated to the underlying calls (a VFun?). I
hope this is doing the same.
The suggestion to use a tclOR is from P.-M. Pédrot.
Note: this is not fully ideal, the messages which were expecting a
trace should be rethought to take into account either that the calls
are not printed anymore, or to print them again.
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.
We have some timeouts in the strategy success file. We should not run
into issues, because we are not really testing how long these take. We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.
Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.
One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556
Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
|
|
|
|
multiple scopes for the same inductive)
|
|
Reviewed-by: maximedenes
|
|
Part of the plan of #11840.
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
|
|
|
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
The real list is computed by tok_using in CLexer.
|
|
Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.
Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
|
|
Reviewed-by: gares
|
|
|
|
|
|
|
|
We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
|
|
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
