| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We avoid using global-access primitives and instead rely on purely functional
passing of the relevant data. Namely, we replace the goal argument with its
environment, and we pass the additional check parameter.
|
|
They were not used anywhere anymore.
|
|
This is already protected by then enter block.
|
|
|
|
This was useless, since we did not observe the difference on evars.
|
|
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: Zimmi48
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: JasonGross
|
|
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
|
|
Reviewed-by: kyoDralliam
|
|
Reviewed-by: MSoegtropIMC
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
|
|
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18.
We instead add a warning in the manual and a kludge in the test-suite.
|
|
We need to record the transparency information in the libobject stack in
order for coqchk to not trip over the strategy information.
This is quite sketchy, though.
|
|
Copy tclWRAPFINALLY to tactics.ml
As per https://github.com/coq/coq/pull/12197#discussion_r418480525 and
https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't export
it from Proofview, because it seems somehow not primitive enough. But
we don't export it from Tactics because it is more of a tactical than a
tactic. But we don't export it from Tacticals because all of the
non-New tacticals there operate on `tactic`, not `Proofview.tactic`, and
all of the `New` tacticals that deal with multi-success things are
focussing, i.e., apply their arguments on each goal separately (and it
even says so in the comment on `New`), whereas it's important that
`tclWRAPFINALLY` doesn't introduce extra focussing.
|
|
|
|
This is the bug
https://github.com/coq/coq/pull/12129#issuecomment-619613779
|
|
As per https://github.com/coq/coq/pull/12129#issuecomment-619389803
Note that we need to work around #12179 in doc of with_strategy
|
|
|
|
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>
|
|
Add real numbers up to 10
|
|
|
|
|
|
multiple scopes for the same inductive)
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
Reviewed-by: cpitclaudel
|
|
Reviewed-by: pi8027
Reviewed-by: zeldovich
|
|
|
|
Part of the plan of #11840.
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ppedrot
|
|
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
|
