diff options
| author | Gaëtan Gilbert | 2019-05-02 19:46:02 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-06-04 13:58:42 +0200 |
| commit | 8abacf00c6c39ec98085d531737d18edc9c19b2a (patch) | |
| tree | 52127cb4b3909e94e53996cd9e170de1f2ea6726 /user-contrib | |
| parent | 1c228b648cb1755cad3ec1f38690110d6fe14bc5 (diff) | |
Proof_global: pass only 1 pstate when we don't want the proof stack
Typically instead of [start_proof : ontop:Proof_global.t option -> bla ->
Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and
the pstate is pushed on the stack by a caller around the
vernacentries/mlg level.
Naming can be a bit awkward, hopefully it can be improved (maybe in a
followup PR).
We can see some patterns appear waiting for nicer combinators, eg in
mlg we often only want to work with the current proof, not the stack.
Behaviour should be similar modulo bugs, let's see what CI says.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 2 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 890ed76d52..49c547a979 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -891,7 +891,7 @@ let classify_ltac2 = function VERNAC COMMAND EXTEND VernacDeclareTactic2Definition | #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> { - fun ~pstate -> Tac2entries.register_struct ?local ~pstate e; pstate + fun ~pstate -> Tac2entries.register_struct ?local ~pstate:(Option.map Proof_global.get_current_pstate pstate) e; pstate } END diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli index d493192bb3..e02c126e71 100644 --- a/user-contrib/Ltac2/tac2entries.mli +++ b/user-contrib/Ltac2/tac2entries.mli @@ -23,7 +23,7 @@ val register_primitive : ?local:bool -> val register_struct : ?local:bool - -> pstate:Proof_global.t option + -> pstate:Proof_global.pstate option -> strexpr -> unit |