Merge PR #6197: [plugin] Remove LocalityFixme über hack.

9 files changed, 94 insertions, 44 deletions

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 1e7da3250..938bec25b 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -65,11 +65,14 @@ let default_intuition_tac =
 let (set_default_solver, default_solver, print_default_solver) = 
   Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver"
 
-VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> [
-    set_default_solver 
-      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (Tacintern.glob_tactic t) ]
+    fun ~atts ~st -> let open Vernacinterp in
+      set_default_solver
+        (Locality.make_section_locality atts.locality)
+        (Tacintern.glob_tactic t);
+        st
+  ]
 END
 
 VERNAC COMMAND EXTEND Firstorder_Print_Solver CLASSIFIED AS QUERY
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 71db919ef..d6cfa3cf9 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -320,24 +320,44 @@ let project_hint pri l2r r =
   let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
-let add_hints_iff l2r lc n bl =
-  let l = Locality.LocalityFixme.consume () in
-  Hints.add_hints (Locality.make_module_locality l) bl
+let add_hints_iff ?locality l2r lc n bl =
+  Hints.add_hints (Locality.make_module_locality locality) bl
     (Hints.HintsResolveEntry (List.map (project_hint n l2r) lc))
 
-VERNAC COMMAND EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
-  [ add_hints_iff true lc n bl ]
+  [ fun ~atts ~st -> begin
+        let open Vernacinterp in
+        add_hints_iff ?locality:atts.locality true lc n bl;
+        st
+      end
+  ]
 | [ "Hint" "Resolve" "->" ne_global_list(lc) natural_opt(n) ] ->
-  [ add_hints_iff true lc n ["core"] ]
+  [ fun ~atts ~st -> begin
+        let open Vernacinterp in
+        add_hints_iff ?locality:atts.locality true lc n ["core"];
+        st
+      end
+  ]
 END
-VERNAC COMMAND EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
+
+VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffRL CLASSIFIED AS SIDEFF
   [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n)
     ":" preident_list(bl) ] ->
-  [ add_hints_iff false lc n bl ]
+  [ fun ~atts ~st -> begin
+        let open Vernacinterp in
+        add_hints_iff ?locality:atts.locality false lc n bl;
+        st
+      end
+  ]
 | [ "Hint" "Resolve" "<-" ne_global_list(lc) natural_opt(n) ] ->
-  [ add_hints_iff false lc n ["core"] ]
+  [ fun ~atts ~st -> begin
+        let open Vernacinterp in
+        add_hints_iff ?locality:atts.locality false lc n ["core"];
+        st
+      end
+  ]
 END
 
 (**********************************************************************)
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 84e79d8ab..90a44708f 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -190,7 +190,7 @@ END
 let pr_hints_path prc prx pry c = Hints.pp_hints_path c
 let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c
 let glob_hints_path ist = Hints.glob_hints_path
-							      
+
 ARGUMENT EXTEND hints_path
 PRINTED BY pr_hints_path
 
@@ -214,10 +214,15 @@ ARGUMENT EXTEND opthints
 | [ ] -> [ None ]
 END
 
-VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [
-  let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
-    Hints.add_hints (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (match dbnames with None -> ["core"] | Some l -> l) entry ]
+    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)
+          (match dbnames with None -> ["core"] | Some l -> l) entry;
+        st
+      end
+ ]
 END
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 116152568..34fea6175 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -469,13 +469,13 @@ VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
   [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ]
 END
 
-VERNAC COMMAND EXTEND VernacTacticNotation
+VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
   [ VtUnknown, VtNow ] ->
-  [
-    let l = Locality.LocalityFixme.consume () in
-    let n = Option.default 0 n in
-    Tacentries.add_tactic_notation (Locality.make_module_locality l) n r e
+  [ fun ~atts ~st -> let open Vernacinterp in
+      let n = Option.default 0 n in
+      Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n r e;
+      st
   ]
 END
 
@@ -512,15 +512,15 @@ PRINTED BY pr_tacdef_body
 | [ tacdef_body(t) ] -> [ t ]
 END
 
-VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
+VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition
 | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [
     VtSideff (List.map (function
       | TacticDefinition ((_,r),_) -> r
       | TacticRedefinition (Ident (_,r),_) -> r
       | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater
-  ] -> [
-    let lc = Locality.LocalityFixme.consume () in
-    Tacentries.register_ltac (Locality.make_module_locality lc) l
+  ] -> [ fun ~atts ~st -> let open Vernacinterp in
+           Tacentries.register_ltac (Locality.make_module_locality atts.locality) l;
+           st
   ]
 END
 
diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4
index fea9e837b..f6cc3833a 100644
--- a/plugins/ltac/g_obligations.ml4
+++ b/plugins/ltac/g_obligations.ml4
@@ -123,11 +123,15 @@ VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF
 | [ "Admit" "Obligations" ] -> [ admit_obligations None ]
 END
 
-VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> [
-    set_default_tactic
-      (Locality.make_section_locality (Locality.LocalityFixme.consume ()))
-      (Tacintern.glob_tactic t) ]
+    fun ~atts ~st -> begin
+        let open Vernacinterp in
+        set_default_tactic
+          (Locality.make_section_locality atts.locality)
+          (Tacintern.glob_tactic t);
+        st
+      end]
 END
 
 open Pp
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index 91abe1019..ea1808a25 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -243,22 +243,37 @@ VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
       [ declare_relation ~binders:b a aeq n None None (Some lemma3) ]
 END
 
-VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
    [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [ add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] a aeq t n ]
+     [ fun ~atts ~st -> let open Vernacinterp in
+         add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
+         st
+     ]
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     [  add_setoid (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders a aeq t n ]
+     [ fun ~atts ~st -> let open Vernacinterp in
+         add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
+         st
+     ]
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ]
-    -> [ add_morphism_infer (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) m n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
+           st
+       ]
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) [] m s n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
+           st
+       ]
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ]
-    -> [ add_morphism (not (Locality.make_section_locality (Locality.LocalityFixme.consume ()))) binders m s n ]
+    -> [ fun ~atts ~st -> let open Vernacinterp in
+           add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
+           st
+       ]
 END
 
 TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c63492d1b..14b0742a7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1800,9 +1800,9 @@ let declare_instance_trans global binders a aeq n lemma =
   in anew_instance global binders instance
        [(Ident (Loc.tag @@ Id.of_string "transitivity"),lemma)]
 
-let declare_relation ?(binders=[]) a aeq n refl symm trans =
+let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans =
   init_setoid ();
-  let global = not (Locality.make_section_locality (Locality.LocalityFixme.consume ())) in
+  let global = not (Locality.make_section_locality locality) in
   let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation"
   in ignore(anew_instance global binders instance []);
   match (refl,symm,trans) with
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 1306c590b..17e7244b3 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -75,7 +75,7 @@ val cl_rewrite_clause :
 val is_applied_rewrite_relation :
   env -> evar_map -> rel_context -> constr -> types option
 
-val declare_relation :
+val declare_relation : ?locality:bool ->
   ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
   constr_expr option -> constr_expr option -> constr_expr option -> unit
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index cd614fee9..7385ed84c 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -158,11 +158,14 @@ let declare_one_prenex_implicit locality f =
   | impls ->
     Impargs.declare_manual_implicits locality fref ~enriching:false [impls]
 
-VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
+VERNAC COMMAND FUNCTIONAL EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
   | [ "Prenex" "Implicits" ne_global_list(fl) ]
-  -> [ let locality =
-         Locality.make_section_locality (Locality.LocalityFixme.consume ()) in
-       List.iter (declare_one_prenex_implicit locality) fl ]
+  -> [ fun ~atts ~st ->
+         let open Vernacinterp in
+         let locality = Locality.make_section_locality atts.locality in
+         List.iter (declare_one_prenex_implicit locality) fl;
+         st
+     ]
 END
 
 (* Vernac grammar visibility patch *)