diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 6189bb18cc..ac65495fe5 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -841,8 +841,8 @@ END let _ = let mode = { Proof_global.name = "Ltac2"; - set = (fun () -> set_command_entry tac2mode); - reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + set = (fun () -> Pvernac.set_command_entry tac2mode); + reset = (fun () -> Pvernac.(set_command_entry Vernac_.noedit_mode)); } in Proof_global.register_proof_mode mode |