diff options
| -rw-r--r-- | src/g_ltac2.mlg | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/g_ltac2.mlg b/src/g_ltac2.mlg index 7020ca079e..c707a82e5b 100644 --- a/src/g_ltac2.mlg +++ b/src/g_ltac2.mlg @@ -897,13 +897,7 @@ END { -let _ = - let mode = { - Proof_global.name = "Ltac2"; - set = (fun () -> Pvernac.set_command_entry tac2mode); - reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode)); - } in - Proof_global.register_proof_mode mode +let _ = Pvernac.register_proof_mode "Ltac2" tac2mode } |