| Age | Commit message (Collapse) | Author |
|---|
|
Fixes #12196
|
|
This new primitive (which could be implemented in terms of `tclCASE`,
but which I believe encapsulates a useful unit of behavior) is needed
for correctly implementing both `with_strategy` and for implementing
multi-success support for the Ltac Profiler.
The basic function of this tactical is to allow wrapping multi-success
tactics with initialization and cleanup routines. For example, if `tac`
is a multi-success tactic that writes its status to a log file, you
might want to wrap `tac` in "first open the log file" and then after it
runs "finally close the log file". (Unfortunately, the way the monad is
set up doesn't allow passing data from the most recent run of the
initializer to the tactic, which suggests that perhaps there's something
a bit off about this abstraction. Perhaps we should set up a ref cell
and that will hold the most recent return of the initializer and pass
this ref cell to the wrapped tactic? But this can be done externally
without needing to modify the current API. In any case, such data is
not needed in the case of the Ltac Profiler, where the initializer is
"update the current call stack and record the current start time" and
the finalizer is "update the call stack and record the end time", and
you want to have the start time be restarted when re-entering a tactic.
Nor is it needed for `with_strategy` which needs to update the global
conv_oracle so that it plays nicely with `abstract`.)
|
|
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: ejgallego
|
|
not lablgtksourceview
Reviewed-by: ejgallego
|
|
Force Cauchy modulus equal to identity, make division transparent
Fix test
|
|
|
|
Reviewed-by: vbgl
|
|
|
|
Reviewed-by: ejgallego
|
|
Nat.le, Nat.lt and Nat.eq are aliased to le, lt and @eq nat.
The required declarations are now added in ZifyInst.
|
|
Reviewed-by: ppedrot
|
|
Some comments referred to the old way of redeclaring constants at section
closure. One of the comments was almost 20 years old...
|
|
accelerate it
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: Zimmi48
Ack-by: rnrand
|
|
I gave preference to the email address with the larger number of
commits.
To find duplicates, I used the script
```bash
for i in $(git shortlog -nse | sed s'/^\s*[0-9]*\s*//g' | grep -o '^[^<]*' | sed s'/\s*$//g' | sed s'/ /,/g'); do if [ $(git shortlog -nse | sed s'/ /,/g' | grep -c "$i") -gt 1 ]; then git shortlog -nse | grep "$(echo "$i" | sed s'/,/ /g')"; fi; done
```
|
|
|
|
Reviewed-by: ejgallego
|
|
in record tuples
Reviewed-by: ejgallego
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
index
Ack-by: Zimmi48
|
|
Reviewed-by: mattam82
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
with an index
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
This encapsulates better the invariants of this function.
|
|
It was trying to warn the user about missing schemes. Since find_scheme was
generating those constants anyways, this was never reached.
|
|
|
|
Ack-by: ejgallego
Ack-by: ppedrot
|
|
This is actually supported by Sphinx directly.
|
|
The convention in the dune build is to be silent except for warnings
and errors, so they don't go unnoticed.
We could have this controlled by a variable if needed (likely would
require some support from Dune?)
Solves part of #12194
|
|
Reviewed-by: SkySkimmer
Reviewed-by: jfehrle
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
Instead, we register functions dynamically declaring the dependencies of the
scheme to be generated.
We had to fix the test-suite because an internal scheme name changed.
We could also tweak the internal flag of scheme dependencies, but in this
particular case it looks more like a bug from the previous implementation.
|
|
Reviewed-by: ejgallego
Reviewed-by: jfehrle
|
|
requiring libraries
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Close #12192
Also removed transforming arbitrary exceptions into Faulty to make it
easier to reason about exception flow
|
|
Ack-by: JasonGross
Ack-by: Zimmi48
Ack-by: cpitclaudel
|
|
After #12023 broke the bug minimizer, I'd like to add
[coq-tools](https://github.com/JasonGross/coq-tools/) to the CI. It's
relatively light-weight (under 5 minutes, I believe), and I'd like to
know when it's going to break on master before it's broken, rather than
after. It tests a relatively under-tested part of Coq, mostly (the
display output of error message, by and large), and I'm happy to take
responsibility for fixing it when some PR is going to break it (mainly I
just want a sort-of early warning system, and I want PRs to not
accidentally break it by changing things that they don't realize they're
changing).
|
|
Reviewed-by: anton-trunov
Reviewed-by: ppedrot
|
|
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
