Adapt to Coq's new proof mode API

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
 
 }