Move attributes out of vernacinterp to new attributes module

12 files changed, 24 insertions, 30 deletions

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index c41687e721..5a4cda54b2 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -74,7 +74,7 @@ let (set_default_solver, default_solver, print_default_solver) =
 
 VERNAC COMMAND EXTEND Firstorder_Set_Solver CLASSIFIED AS SIDEFF
 | [ "Set" "Firstorder" "Solver" tactic(t) ] -> {
-    let open Vernacinterp in
+    let open Attributes in
       set_default_solver
         (Locality.make_section_locality atts.locality)
         (Tacintern.glob_tactic t)
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index b660865e8b..11b970d2ef 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -30,7 +30,7 @@ open Namegen
 open Tactypes
 open Tactics
 open Proofview.Notations
-open Vernacinterp
+open Attributes
 
 let wit_hyp = wit_var
 
@@ -414,12 +414,10 @@ VERNAC COMMAND EXTEND DeriveInversionClear
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac }
 
 | [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac }
 END
 
@@ -427,12 +425,10 @@ VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac }
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac }
 END
 
@@ -440,7 +436,6 @@ VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac }
 END
 
@@ -448,7 +443,6 @@ VERNAC COMMAND EXTEND DeriveDependentInversionClear
 | [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ]
   => { seff na }
   -> {
-      let open Vernacinterp in
       add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac }
 END
 
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index c07b653f3a..65fa34d712 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -240,7 +240,7 @@ END
 
 VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF
 | [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> {
-        let open Vernacinterp in
+        let open Attributes in
         let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
         Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
           (match dbnames with None -> ["core"] | Some l -> l) entry;
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d62f985350..f1f3ae74e5 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -500,7 +500,7 @@ END
 VERNAC COMMAND EXTEND VernacTacticNotation
 | [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] =>
   { VtSideff [], VtNow } ->
-  { let open Vernacinterp in
+  { let open Attributes in
       let n = Option.default 0 n in
       let deprecation = atts.deprecated in
       Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e;
@@ -549,7 +549,7 @@ VERNAC COMMAND EXTEND VernacDeclareTacticDefinition
     VtSideff (List.map (function
       | TacticDefinition ({CAst.v=r},_) -> r
       | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater
-  } -> { let open Vernacinterp in
+  } -> { let open Attributes in
            let deprecation = atts.deprecated in
            Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l;
   }
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index 26f2b08d3a..32dccf2e83 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -132,9 +132,8 @@ END
 
 VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF
 | [ "Obligation" "Tactic" ":=" tactic(t) ] -> {
-        let open Vernacinterp in
         set_default_tactic
-          (Locality.make_section_locality atts.locality)
+          (Locality.make_section_locality atts.Attributes.locality)
           (Tacintern.glob_tactic t);
   }
 END
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 3e47724c4c..3f12e0e9f9 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -26,6 +26,7 @@ open Pcoq.Prim
 open Pcoq.Constr
 open Pvernac.Vernac_
 open Pltac
+open Attributes
 
 let wit_hyp = wit_var
 
@@ -271,28 +272,28 @@ END
 
 VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
   | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     { let open Vernacinterp in
+     {
          add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n;
      }
   | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
-     { let open Vernacinterp in
+     {
          add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n;
      }
   | [ "Add" "Morphism" constr(m) ":" ident(n) ]
     (* This command may or may not open a goal *)
     => { Vernacexpr.VtUnknown, Vernacexpr.VtNow }
-    -> { let open Vernacinterp in
+    -> {
            add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n;
        }
   | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-    -> { let open Vernacinterp in
+    -> {
            add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n;
        }
   | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
         "with" "signature" lconstr(s) "as" ident(n) ]
     => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) }
-    -> { let open Vernacinterp in
+    -> {
            add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n;
        }
 END
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 5b4bedb50a..c93d6251e0 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -12,7 +12,7 @@
 
 open Vernacexpr
 open Tacexpr
-open Vernacinterp
+open Attributes
 
 (** {5 Tactic Definitions} *)
 
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index a88285c9ee..d5f22b2c72 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -55,7 +55,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: Attributes.deprecation option;
   }
 
 let alias_map = Summary.ref ~name:"tactic-alias"
@@ -121,7 +121,7 @@ type ltac_entry = {
   tac_for_ml : bool;
   tac_body : glob_tactic_expr;
   tac_redef : ModPath.t list;
-  tac_deprecation : Vernacinterp.deprecation option
+  tac_deprecation : Attributes.deprecation option
 }
 
 let mactab =
@@ -178,7 +178,7 @@ let subst_md (subst, (local, id, b, t, deprecation)) =
 let classify_md (local, _, _, _, _ as o) = Substitute o
 
 let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
-           Vernacinterp.deprecation option -> obj =
+           Attributes.deprecation option -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
diff --git a/plugins/ltac/tacenv.mli b/plugins/ltac/tacenv.mli
index d5d36c97fa..5b98daf383 100644
--- a/plugins/ltac/tacenv.mli
+++ b/plugins/ltac/tacenv.mli
@@ -12,7 +12,7 @@ open Names
 open Libnames
 open Tacexpr
 open Geninterp
-open Vernacinterp
+open Attributes
 
 (** This module centralizes the various ways of registering tactics. *)
 
@@ -33,7 +33,7 @@ type alias = KerName.t
 type alias_tactic =
   { alias_args: Id.t list;
     alias_body: glob_tactic_expr;
-    alias_deprecation: Vernacinterp.deprecation option;
+    alias_deprecation: deprecation option;
   }
 (** Contents of a tactic notation *)
 
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index fcbcfae115..fce1d54d8c 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -121,15 +121,15 @@ let warn_deprecated_tactic =
   CWarnings.create ~name:"deprecated-tactic" ~category:"deprecated"
     (fun (qid,depr) -> str "Tactic " ++ pr_qualid qid ++
       strbrk " is deprecated" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let warn_deprecated_alias =
   CWarnings.create ~name:"deprecated-tactic-notation" ~category:"deprecated"
     (fun (kn,depr) -> str "Tactic Notation " ++ Pptactic.pr_alias_key kn ++
       strbrk " is deprecated since" ++
-      pr_opt (fun since -> str "since " ++ str since) depr.Vernacinterp.since ++
-      str "." ++ pr_opt (fun note -> str note) depr.Vernacinterp.note)
+      pr_opt (fun since -> str "since " ++ str since) depr.Attributes.since ++
+      str "." ++ pr_opt (fun note -> str note) depr.Attributes.note)
 
 let intern_isolated_global_tactic_reference qid =
   let loc = qid.CAst.loc in
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 940defb743..2f44624d36 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -172,7 +172,7 @@ let declare_one_prenex_implicit locality f =
 VERNAC COMMAND EXTEND Ssrpreneximplicits CLASSIFIED AS SIDEFF
   | [ "Prenex" "Implicits" ne_global_list(fl) ]
   -> {
-         let open Vernacinterp in
+         let open Attributes in
          let locality = Locality.make_section_locality atts.locality in
          List.iter (declare_one_prenex_implicit locality) fl;
      }
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 5dbc9eea7a..54764d541f 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -16,7 +16,7 @@ open Notation
 open Numeral
 open Pp
 open Names
-open Vernacinterp
+open Attributes
 open Ltac_plugin
 open Stdarg
 open Pcoq.Prim