diff options
| author | Jason Gross | 2020-04-19 17:37:27 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-09 13:01:02 -0400 |
| commit | 2edbbfee7fdcfb2a4804524091930c5dab7b9db4 (patch) | |
| tree | 4eabc42b9df77c2ed12b344049e859e9b64af52e /interp | |
| parent | 5681ea2535bbaef18e55d9bdc4270e12856de114 (diff) | |
Add a `with_strategy` tactic
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>
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/stdarg.ml | 2 | ||||
| -rw-r--r-- | interp/stdarg.mli | 2 |
2 files changed, 4 insertions, 0 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 492671fff0..d5f104b7f8 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -42,6 +42,8 @@ let wit_var = let wit_ref = make0 "ref" +let wit_smart_global = make0 ~dyn:(val_tag (topwit wit_ref)) "smart_global" + let wit_sort_family = make0 "sort_family" let wit_constr = diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 35de3693cb..89bdd78c70 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -39,6 +39,8 @@ val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_smart_global : (qualid or_by_notation, GlobRef.t located or_var, GlobRef.t) genarg_type + val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type |