Move attributes out of vernacinterp to new attributes module

20 files changed, 86 insertions, 73 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
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 85babd922b..b393093601 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,8 +194,8 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
-      let poly = atts.Vernacinterp.polymorphic in
+      let _, atts = Vernacentries.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in
+      let poly = atts.Attributes.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
new file mode 100644
index 0000000000..2f1f6e04e3
--- /dev/null
+++ b/vernac/attributes.ml
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type deprecation = { since : string option ; note : string option }
+
+let mk_deprecation ?(since=None) ?(note=None) () =
+  { since ; note }
+
+type t = {
+  loc : Loc.t option;
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  program : bool;
+  deprecated : deprecation option;
+}
+
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () =
+  { loc ; locality ; polymorphic ; program ; deprecated; template }
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
new file mode 100644
index 0000000000..571f0ddd7d
--- /dev/null
+++ b/vernac/attributes.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type deprecation = { since : string option ; note : string option }
+
+val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
+
+type t = {
+  loc : Loc.t option;
+  locality : bool option;
+  polymorphic : bool;
+  template : bool option;
+  program : bool;
+  deprecated : deprecation option;
+}
+
+val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+  ?polymorphic: bool -> ?template:bool option ->
+  ?program: bool -> ?deprecated: deprecation option -> unit -> t
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 356951b695..35ce8c726b 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -7,6 +7,7 @@ Himsg
 ExplainErr
 Locality
 Egramml
+Attributes
 Vernacinterp
 Ppvernac
 Proof_using
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1190d73258..391e8f7990 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -31,6 +31,7 @@ open Redexpr
 open Lemmas
 open Locality
 open Vernacinterp
+open Attributes
 
 module NamedDecl = Context.Named.Declaration
 
@@ -2109,7 +2110,6 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
-  let open Vernacinterp in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
 
@@ -2505,7 +2505,7 @@ open Extend
 type classifier = Genarg.raw_generic_argument list -> vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
 
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 0c4630e45f..f533dd25f4 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,14 +41,14 @@ val universe_polymorphism_option_name : string list
 
 (** Elaborate a [atts] record out of a list of flags.
     Also returns whether polymorphism is explicitly (un)set. *)
-val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+val attributes_of_flags : Vernacexpr.vernac_flags -> Attributes.t -> bool option * Attributes.t
 
 (** {5 VERNAC EXTEND} *)
 
 type classifier = Genarg.raw_generic_argument list -> Vernacexpr.vernac_classification
 
 type (_, _) ty_sig =
-| TyNil : (atts:Vernacinterp.atts -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
+| TyNil : (atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t, Vernacexpr.vernac_classification) ty_sig
 | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
 | TyNonTerminal :
   ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig ->
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 2746cbd144..b16784eb22 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,24 +12,7 @@ open Util
 open Pp
 open CErrors
 
-type deprecation = { since : string option ; note : string option }
-
-let mk_deprecation ?(since=None) ?(note=None) () =
-  { since ; note }
-
-type atts = {
-  loc : Loc.t option;
-  locality : bool option;
-  polymorphic : bool;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(template=None) ?(program=false) ?(deprecated=None) () : atts =
-  { loc ; locality ; polymorphic ; program ; deprecated; template }
-
-type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 62a178b555..ba3d911810 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,24 +10,7 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type deprecation = { since : string option ; note : string option }
-
-val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
-
-type atts = {
-  loc : Loc.t option;
-  locality : bool option;
-  polymorphic : bool;
-  template : bool option;
-  program : bool;
-  deprecated : deprecation option;
-}
-
-val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
-  ?polymorphic: bool -> ?template:bool option ->
-  ?program: bool -> ?deprecated: deprecation option -> unit -> atts
-
-type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+type 'a vernac_command = 'a -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -35,4 +18,4 @@ val vinterp_init : unit -> unit
 val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
-val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
+val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.t -> st:Vernacstate.t -> Vernacstate.t