| Age | Commit message (Collapse) | Author |
|---|
|
indirectly dependent in goal
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
|
|
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.
|
|
|
|
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>
|
|
|
|
This is saner behavior making subst reversible, as discussed in #12139.
This also fixes #10812 and #12139.
In passing, we also simplify a bit the code of "subst_all".
|
|
|
|
This function was used almost everywhere with the wrapper around.
|
|
This encapsulates better the invariants of this function.
|
|
|
|
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: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
custom induction scheme
Reviewed-by: ppedrot
|
|
Reviewed-by: herbelin
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
|
|
|
|
Rewriter needs a bit of work as it calls a removed function, but no
big deal.
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
It seems to belong there, not in `tactics`
|
|
This makes sense as it is mandatory for the client.
|
|
We mark all the stuff scheduled to disappear in `Declare`, and remove
a couple of non-needed APIs.
|
|
As we are aiming to forbid low-level manipulation of proofs outside
`Declare`, we move the code from `Abstract` to `Declare`.
We remove `build_constant_by_tactic` from the public API.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
This actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
|
|
|
|
|
|
|
|
Old code was doing two passes on `initial_goals`; this produced some
awkward situations code-wise.
The `~unsafe_typ` parameter to `prepare` is needed to preserve the
behavior introduced in bf0499bc507d5a39c3d5e3bf1f69191339270729 :
> Do not normalize the type of a proof according to the final universes
> when keep_body_ucst_separate is true, otherwise the type might not be
> retypable in the initial context
We need to investigate more, as of today we keep this behavior which
seems to work.
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
|
|
As suggested by Gaëtan Gilbert.
|
|
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
|
|
|
|
|
|
After the last refactoring commit, the entry_fn function is redundant
and we can just get rid of it and get a more direct code.
|
|
We do some minor refactoring, removing one-use local definitions, and
cleaning up the `EConstr.t -> Constr.t` path, what is going on with
the use of unsafe it now becomes clear.
|
|
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
|
