diff options
Diffstat (limited to 'plugins/ltac')
-rw-r--r-- | plugins/ltac/extratactics.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/g_ltac.ml4 | 8 | ||||
-rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 2 | ||||
-rw-r--r-- | plugins/ltac/g_tactic.ml4 | 2 |
5 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index c21921513..17011f206 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r = let add_hints_iff ~atts l2r lc n bl = let open Vernacinterp in - Hints.add_hints (Locality.make_module_locality atts.locality) bl + Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl (Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc)) VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 643f7e99f..07047d016 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -219,7 +219,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF fun ~atts ~st -> begin let open Vernacinterp in let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints (Locality.make_section_locality atts.locality) + Hints.add_hints ~local:(Locality.make_section_locality atts.locality) (match dbnames with None -> ["core"] | Some l -> l) entry; st end 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 diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index fbaa2e58f..079001ee4 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -20,9 +20,9 @@ open Extraargs open Tacmach open Rewrite open Stdarg -open Pcoq.Vernac_ open Pcoq.Prim open Pcoq.Constr +open Pvernac.Vernac_ open Pltac DECLARE PLUGIN "ltac_plugin" diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 7534e2799..dc9f607cf 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -211,7 +211,7 @@ let warn_deprecated_eqn_syntax = (* Auxiliary grammar rules *) -open Vernac_ +open Pvernac.Vernac_ GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis |