diff options
Diffstat (limited to 'plugins/ltac/g_ltac.ml4')
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 4857beffa..ed54320a5 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -21,9 +21,9 @@ open Tok (* necessary for camlp5 *) open Names open Pcoq -open Pcoq.Constr -open Pcoq.Vernac_ open Pcoq.Prim +open Pcoq.Constr +open Pvernac.Vernac_ open Pltac let fail_default_value = ArgArg 0 @@ -58,8 +58,8 @@ let tacdef_body = new_entry "tactic:tacdef_body" let _ = let mode = { Proof_global.name = "Classic"; - set = (fun () -> set_command_entry tactic_mode); - reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + set = (fun () -> Pvernac.set_command_entry tactic_mode); + reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); } in Proof_global.register_proof_mode mode |