diff options
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 |