[api] Refactor most of `Decl_kinds`

We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.

The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.

Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.

IMO this needs more work, but this should be a good start.

47 files changed, 266 insertions, 262 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 68ae5628db..9dd4700db5 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -9,4 +9,4 @@ let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
   edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-    ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None []
+    ~kind:Decls.Definition ~opaque:false sigma udecl body None []
diff --git a/library/decls.ml b/interp/decls.ml
index 5cb35323dd..933aa774b4 100644
--- a/library/decls.ml
+++ b/interp/decls.ml
@@ -12,18 +12,69 @@
      associated declarations *)
 
 open Names
-open Decl_kinds
 open Libnames
 
-(** Datas associated to section variables and local definitions *)
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+  | Property
+  | Proposition
+  | Corollary
 
-type variable_data = {
-  path:DirPath.t;
-  opaque:bool;
-  univs:Univ.ContextSet.t;
-  poly:bool;
-  kind:logical_kind;
-}
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
+  | Instance
+  | Method
+  | Let
+
+type assumption_object_kind = Definitional | Logical | Conjectural | Context
+
+(* [assumption_kind]
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+(** Kinds used in proofs *)
+
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
+  | Proof of theorem_kind
+
+(** Kinds used in library *)
+
+type logical_kind =
+  | IsPrimitive
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
+
+let logical_kind_of_goal_kind = function
+  | DefinitionBody d -> IsDefinition d
+  | Proof s -> IsProof s
+
+(** Data associated to section variables and local definitions *)
+
+type variable_data =
+  { path:DirPath.t
+  ; opaque:bool
+  ; univs:Univ.ContextSet.t
+  ; poly:bool
+  ; kind:logical_kind
+  }
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
diff --git a/library/decls.mli b/interp/decls.mli
index f88958bb04..570f03bbce 100644
--- a/library/decls.mli
+++ b/interp/decls.mli
@@ -10,7 +10,57 @@
 
 open Names
 open Libnames
-open Decl_kinds
+
+type theorem_kind =
+  | Theorem
+  | Lemma
+  | Fact
+  | Remark
+  | Property
+  | Proposition
+  | Corollary
+
+type definition_object_kind =
+  | Definition
+  | Coercion
+  | SubClass
+  | CanonicalStructure
+  | Example
+  | Fixpoint
+  | CoFixpoint
+  | Scheme
+  | StructureComponent
+  | IdentityCoercion
+  | Instance
+  | Method
+  | Let
+
+type assumption_object_kind = Definitional | Logical | Conjectural | Context
+
+(* [assumption_kind]
+
+                |  Local      | Global
+   ------------------------------------
+   Definitional |  Variable   | Parameter
+   Logical      |  Hypothesis | Axiom
+
+*)
+(** Kinds used in proofs *)
+
+type goal_object_kind =
+  | DefinitionBody of definition_object_kind
+  | Proof of theorem_kind
+
+(** Kinds used in library *)
+
+type logical_kind =
+  | IsPrimitive
+  | IsAssumption of assumption_object_kind
+  | IsDefinition of definition_object_kind
+  | IsProof of theorem_kind
+
+(** Operations *)
+val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
 
 (** This module manages non-kernel informations about declarations. It
     is either non-logical informations or logical informations that
@@ -18,24 +68,33 @@ open Decl_kinds
 
 (** Registration and access to the table of variable *)
 
-type variable_data = {
-  path:DirPath.t;
-  opaque:bool;
-  univs:Univ.ContextSet.t;
-  poly:bool;
-  kind:logical_kind;
-}
+type variable_data =
+  { path:DirPath.t
+  ; opaque:bool
+  ; univs:Univ.ContextSet.t
+  ; poly:bool
+  ; kind:logical_kind
+  }
 
 val add_variable_data : variable -> variable_data -> unit
+
+(* Not used *)
 val variable_path : variable -> DirPath.t
+
+(* Only used in dumpglob *)
 val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
+
+(* User in Lemma, Very dubious *)
 val variable_opacity : variable -> bool
+
+(* Used in declare, very dubious *)
 val variable_context : variable -> Univ.ContextSet.t
 val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
 
+(* Only used in dumpglob *)
 val add_constant_kind : Constant.t -> logical_kind -> unit
 val constant_kind : Constant.t -> logical_kind
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index e1269025a4..53baf137cf 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -69,7 +69,7 @@ let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
-open Decl_kinds
+open Decls
 open Declarations
 
 let type_of_logical_kind = function
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 33573edcce..cb6c527c83 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -10,6 +10,7 @@ Notation
 Syntax_def
 Smartlocate
 Constrexpr_ops
+Decls
 Dumpglob
 Reserve
 Impargs
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 6eb582baef..5c479255df 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -15,51 +15,3 @@ type binding_kind = Explicit | Implicit
 type private_flag = bool
 
 type cumulative_inductive_flag = bool
-
-type theorem_kind =
-  | Theorem
-  | Lemma
-  | Fact
-  | Remark
-  | Property
-  | Proposition
-  | Corollary
-
-type definition_object_kind =
-  | Definition
-  | Coercion
-  | SubClass
-  | CanonicalStructure
-  | Example
-  | Fixpoint
-  | CoFixpoint
-  | Scheme
-  | StructureComponent
-  | IdentityCoercion
-  | Instance
-  | Method
-  | Let
-
-type assumption_object_kind = Definitional | Logical | Conjectural | Context
-
-(* [assumption_kind]
-
-                |  Local      | Global
-   ------------------------------------
-   Definitional |  Variable   | Parameter
-   Logical      |  Hypothesis | Axiom
-
-*)
-(** Kinds used in proofs *)
-
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
-
-(** Kinds used in library *)
-
-type logical_kind =
-  | IsPrimitive
-  | IsAssumption of assumption_object_kind
-  | IsDefinition of definition_object_kind
-  | IsProof of theorem_kind
diff --git a/library/kindops.ml b/library/kindops.ml
deleted file mode 100644
index 0bf55c62a9..0000000000
--- a/library/kindops.ml
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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)         *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-let logical_kind_of_goal_kind = function
-  | DefinitionBody d -> IsDefinition d
-  | Proof s -> IsProof s
-
-let string_of_theorem_kind = function
-  | Theorem -> "Theorem"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Remark -> "Remark"
-  | Property -> "Property"
-  | Proposition -> "Proposition"
-  | Corollary -> "Corollary"
-
-let string_of_definition_object_kind = function
-  | Definition -> "Definition"
-  | Example -> "Example"
-  | Coercion -> "Coercion"
-  | SubClass -> "SubClass"
-  | CanonicalStructure -> "Canonical Structure"
-  | Instance -> "Instance"
-  | Let -> "Let"
-  | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
-    CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/kindops.mli b/library/kindops.mli
deleted file mode 100644
index 3c9f2bb7c3..0000000000
--- a/library/kindops.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <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)         *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
-val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_object_kind : definition_object_kind -> string
diff --git a/library/library.mllib b/library/library.mllib
index ef53471377..35af5fa43b 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,16 +1,15 @@
+Decl_kinds
 Libnames
 Globnames
 Libobject
 Summary
 Nametab
 Global
-Decl_kinds
 Lib
 Declaremods
 Library
 States
 Kindops
 Goptions
-Decls
 Keys
 Coqlib
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e34150f2b3..780cf4af21 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -20,7 +20,7 @@ let start_deriving f suchthat name : Lemmas.t =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let poly = false in
-  let kind = Decl_kinds.(DefinitionBody Definition) in
+  let kind = Decls.(DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f773b2c39e..6a5307d8f5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
   let info = Lemmas.Info.make
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+      ~kind:(Decls.(Proof Theorem)) () in
 
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3bab750534..87910eeae7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -371,7 +371,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
           Declare.declare_constant
             name
             (Declare.DefinitionEntry ce,
-             Decl_kinds.IsDefinition (Decl_kinds.Scheme))
+             Decls.(IsDefinition Scheme))
         );
         Declare.definition_message name;
         names := name :: !names
@@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -638,7 +638,7 @@ let build_scheme fas =
        ignore
          (Declare.declare_constant
             princ_id
-            (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+            (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem)));
        Declare.definition_message princ_id
     )
     fas
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d305a58ccc..9a9e0b9692 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
         ~name:fname
         ~poly:false
         ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-        ~kind:Decl_kinds.Definition pl
+        ~kind:Decls.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 56ed406e2f..b32b27ebeb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -127,13 +127,13 @@ let save id const ?hook uctx scope kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match scope with
     | Discharge ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Decls.logical_kind_of_goal_kind kind in
         let c = SectionLocalDef const in
         let _ = declare_variable id (Lib.cwd(), c, k) in
         VarRef id
     | Global local ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
-        let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
+        let k = Decls.logical_kind_of_goal_kind kind in
+        let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
   DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 45d332031f..1758efe584 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -48,7 +48,7 @@ val save
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> DeclareDef.locality
-  -> Decl_kinds.goal_object_kind
+  -> Decls.goal_object_kind
   -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 86defb2f2f..153b27c855 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let (typ,_) = lemmas_types_infos.(i) in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+             ~kind:(Decls.(Proof Theorem)) () in
          let lemma = Lemmas.start_lemma
              ~name:lem_id
              ~poly:false
@@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          let lem_id = mk_complete_id f_id in
          let info = Lemmas.Info.make
              ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
-             ~kind:Decl_kinds.(Proof Theorem) () in
+             ~kind:Decls.(Proof Theorem) () in
          let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
              sigma (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d38e28c0e7..0398acf242 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -30,7 +30,6 @@ open Tacmach
 open Tactics
 open Nametab
 open Declare
-open Decl_kinds
 open Tacred
 open Goal
 open Glob_term
@@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
     let body = EConstr.Unsafe.to_constr body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
+let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
   let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(Proof Lemma))
       () in
   let lemma = Lemmas.start_lemma
       ~name:na
@@ -1411,7 +1410,7 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(Proof Lemma) () in
     let lemma = Lemmas.start_lemma ~name:thm_name
         ~poly:false (*FIXME*)
         ~sign:(Environ.named_context_val env)
@@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref =
     let univs = Evd.univ_entry ~poly:false evd in
-    declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
+    declare_fun functional_id Decls.(IsDefinition Definition) ~univs res
   in
   (* Refresh the global universes, now including those of _F *)
   let evd = Evd.from_env (Global.env ()) in
@@ -1549,7 +1548,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
   let hook { DeclareDef.Hook.S.uctx ; _ } =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
-    let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+    let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in
     let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
     (*     message "start second proof"; *)
     let stop =
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 19866df8e3..22ad75b784 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1901,8 +1901,8 @@ let declare_projection n instance_id r =
   let cst = 
     Declare.definition_entry ~types:typ ~univs term
   in
-    ignore(Declare.declare_constant n 
-           (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+    ignore(Declare.declare_constant n
+           (Declare.DefinitionEntry cst, Decls.(IsDefinition Definition)))
 
 let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1981,7 +1981,7 @@ let add_morphism_as_parameter atts m n : unit =
   let cst = Declare.declare_constant instance_id
       (Declare.ParameterEntry
          (None,(instance,uctx),None),
-       Decl_kinds.IsAssumption Decl_kinds.Logical)
+       Decls.(IsAssumption Logical))
   in
   Classes.add_instance (Classes.mk_instance
                   (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
@@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
   let poly = atts.polymorphic in
-  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let kind = Decls.(DefinitionBody Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
     | Globnames.ConstRef cst ->
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 33798c43c8..3d6bfda0b2 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -29,7 +29,6 @@ open Tacinterp
 open Libobject
 open Printer
 open Declare
-open Decl_kinds
 open Entries
 open Newring_ast
 open Proofview.Notations
@@ -158,7 +157,7 @@ let decl_constant na univs c =
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
             (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c),
-	     IsProof Lemma))
+             Decls.(IsProof Lemma)))
 
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 662a2fc22c..56f432ee1d 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -13,7 +13,6 @@ module CVars = Vars
 open Util
 open Termops
 open EConstr
-open Decl_kinds
 open Evarutil
 
 module RelDecl = Context.Rel.Declaration
@@ -153,7 +152,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let const, args = shrink_entry sign const in
   let args = List.map EConstr.of_constr args in
   let cd = Declare.DefinitionEntry { const with Proof_global.proof_entry_opaque = opaque } in
-  let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in
+  let decl = (cd, if opaque then Decls.(IsProof Lemma) else Decls.(IsDefinition Definition)) in
   let cst () =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index aa94ab5a25..b994585e8a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -24,7 +24,6 @@ open Lib
 open Impargs
 open Safe_typing
 open Cooking
-open Decls
 open Decl_kinds
 
 module NamedDecl = Context.Named.Declaration
@@ -36,7 +35,7 @@ type import_status = ImportDefaultBehavior | ImportNeedQualified
 type constant_obj = {
   cst_decl : Cooking.recipe option;
   (** Non-empty only when rebuilding a constant after a section *)
-  cst_kind : logical_kind;
+  cst_kind : Decls.logical_kind;
   cst_locl : import_status;
 }
 
@@ -45,7 +44,7 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type constant_declaration = Evd.side_effects constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
@@ -54,7 +53,7 @@ let load_constant i ((sp,kn), obj) =
     alreadydeclared (Id.print (basename sp) ++ str " already exists");
   let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (ConstRef con);
-  add_constant_kind con obj.cst_kind
+  Decls.add_constant_kind con obj.cst_kind
 
 let cooking_info segment =
   let modlist = replacement_context () in
@@ -73,7 +72,7 @@ let open_constant i ((sp,kn), obj) =
     Nametab.push (Nametab.Exactly i) sp (ConstRef con)
 
 let exists_name id =
-  variable_exists id || Global.exists_objlabel (Label.of_id id)
+  Decls.variable_exists id || Global.exists_objlabel (Label.of_id id)
 
 let check_exists id =
   if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
@@ -95,7 +94,7 @@ let cache_constant ((sp,kn), obj) =
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
   add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
-  add_constant_kind (Constant.make1 kn) obj.cst_kind
+  Decls.add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
   let con = Constant.make1 kn in
@@ -141,7 +140,7 @@ let register_constant kn kind local =
   update_tables kn
 
 let register_side_effect (c, role) =
-  let () = register_constant c (IsProof Theorem) ImportDefaultBehavior in
+  let () = register_constant c Decls.(IsProof Theorem) ImportDefaultBehavior in
   match role with
   | None -> ()
   | Some (Evd.Schema (ind, kind)) -> !declare_scheme kind [|ind,c|]
@@ -294,27 +293,27 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) id (cd, kind
   kn, eff
 
 let declare_definition
-  ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = ImportDefaultBehavior)
+  ?(opaque=false) ?(kind=Decls.Definition) ?(local = ImportDefaultBehavior)
   id ?types (body,univs) =
   let cb =
     definition_entry ?types ~univs ~opaque body
   in
     declare_constant ~local id
-      (DefinitionEntry cb, Decl_kinds.IsDefinition kind)
+      (DefinitionEntry cb, Decls.IsDefinition kind)
 
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
   | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
-type variable_declaration = DirPath.t * section_variable_entry * logical_kind
+type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
   | Inr (id,(path,d,kind)) ->
   (* Constr raisonne sur les noms courts *)
-  if variable_exists id then
+  if Decls.variable_exists id then
     alreadydeclared (Id.print id ++ str " already exists");
 
   let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
@@ -349,12 +348,12 @@ let cache_variable ((sp,_),o) =
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
   add_section_variable ~name:id ~kind:impl ~poly univs;
-  add_variable_data id {path;opaque;univs;poly;kind}
+  Decls.(add_variable_data id {path;opaque;univs;poly;kind})
 
 let discharge_variable (_,o) = match o with
   | Inr (id,_) ->
-    if variable_polymorphic id then None
-    else Some (Inl (variable_context id))
+    if Decls.variable_polymorphic id then None
+    else Some (Inl (Decls.variable_context id))
   | Inl _ -> Some o
 
 type variable_obj =
@@ -491,11 +490,10 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let term = Vars.subst_instance_constr u term in
   let types = Vars.subst_instance_constr u types in
   let entry = definition_entry ~types ~univs term in
-  let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
+  let cst = declare_constant id (DefinitionEntry entry, Decls.(IsDefinition StructureComponent)) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
   declare_primitive_projection p cst
 
-
 let declare_projections univs mind =
   let env = Global.env () in
   let mib = Environ.lookup_mind mind env in
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 1f72fff30e..0fc22f26c4 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -11,7 +11,6 @@
 open Names
 open Constr
 open Entries
-open Decl_kinds
 
 (** This module provides the official functions to declare new variables,
    parameters, constants and inductive types. Using the following functions
@@ -31,14 +30,14 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-type variable_declaration = DirPath.t * section_variable_entry * logical_kind
+type variable_declaration = DirPath.t * section_variable_entry * Decls.logical_kind
 
 val declare_variable : variable -> variable_declaration -> Libobject.object_name
 
 (** Declaration of global constructions
    i.e. Definition/Theorem/Axiom/Parameter/... *)
 
-type constant_declaration = Evd.side_effects constant_entry * logical_kind
+type constant_declaration = Evd.side_effects constant_entry * Decls.logical_kind
 
 (* Default definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
@@ -61,7 +60,7 @@ val declare_private_constant :
   ?role:Evd.side_effect_role -> ?local:import_status -> Id.t -> constant_declaration -> Constant.t * Evd.side_effects
 
 val declare_definition :
-  ?opaque:bool -> ?kind:definition_object_kind ->
+  ?opaque:bool -> ?kind:Decls.definition_object_kind ->
   ?local:import_status -> Id.t -> ?types:constr ->
   constr Entries.in_universes_entry -> Constant.t
 
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index e01f3ab961..29963bc105 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -22,7 +22,6 @@ open Declarations
 open Constr
 open CErrors
 open Util
-open Decl_kinds
 open Pp
 
 (**********************************************************************)
@@ -136,7 +135,7 @@ let define internal role id c poly univs =
     proof_entry_inline_code = false;
     proof_entry_feedback = None;
   } in
-  let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decl_kinds.IsDefinition Scheme) in
+  let kn, eff = Declare.declare_private_constant ~role id (Declare.DefinitionEntry entry, Decls.(IsDefinition Scheme)) in
   let () = match internal with
     | InternalTacticRequest -> ()
     | _-> Declare.definition_message id
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index e242b10d33..2ef06d2246 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -27,7 +27,6 @@ open Tacmach.New
 open Clenv
 open Tacticals.New
 open Tactics
-open Decl_kinds
 open Context.Named.Declaration
 
 module NamedDecl = Context.Named.Declaration
@@ -236,7 +235,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op =
   let invProof, sigma = inversion_scheme ~name ~poly env sigma t sort dep inv_op in
   let univs = Evd.univ_entry ~poly sigma in
   let entry = Declare.definition_entry ~univs invProof in
-  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, IsProof Lemma) in
+  let _ = Declare.declare_constant name (Declare.DefinitionEntry entry, Decls.(IsProof Lemma)) in
   ()
 
 (* inv_op = Inv (derives de complete inv. lemma)
diff --git a/vernac/class.ml b/vernac/class.ml
index 6dba134764..c0d8837c2e 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -21,7 +21,6 @@ open Environ
 open Classops
 open Declare
 open Globnames
-open Decl_kinds
 open Libobject
 
 let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
@@ -222,7 +221,7 @@ let build_id_coercion idf_opt source poly =
       (definition_entry ~types:typ_f ~univs
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
-  let decl = (constr_entry, IsDefinition IdentityCoercion) in
+  let decl = (constr_entry, Decls.(IsDefinition IdentityCoercion)) in
   let kn = declare_constant idf decl in
   ConstRef kn
 
diff --git a/vernac/classes.ml b/vernac/classes.ml
index fbcd1744a8..01fc120af2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -315,7 +315,7 @@ let instance_hook info global imps ?hook cst =
 
 let declare_instance_constant info global imps ?hook id decl poly sigma term termtype =
   (* XXX: Duplication of the declare_constant path *)
-  let kind = IsDefinition Instance in
+  let kind = Decls.(IsDefinition Instance) in
   let sigma =
     let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
                                  (CVars.universes_of_constr term) in
@@ -338,7 +338,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri decl imps subst id
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
   let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
   let cst = Declare.declare_constant id
-      (Declare.ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
+      (Declare.ParameterEntry entry, Decls.(IsAssumption Logical)) in
   Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
   instance_hook pri global imps (ConstRef cst)
 
@@ -363,7 +363,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
   let hook = DeclareDef.Hook.make hook in
   let ctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:id ?term:constr
-           ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
+           ~univdecl:decl ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Decls.Instance ~hook typ ctx obls)
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
@@ -373,7 +373,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
-  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let kind = Decls.(DefinitionBody Instance) in
   let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~scope ~kind () in
   let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e91d8b9d3e..d7ad5133a6 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -18,7 +18,6 @@ open Globnames
 open Constrexpr_ops
 open Constrintern
 open Impargs
-open Decl_kinds
 open Pretyping
 open Entries
 
@@ -36,7 +35,7 @@ let () =
       optread = (fun _ -> !axiom_into_instance);
       optwrite = (:=) axiom_into_instance; }
 
-let should_axiom_into_instance = function
+let should_axiom_into_instance = let open Decls in function
   | Context ->
     (* The typeclass behaviour of Variable and Context doesn't depend
        on section status *)
@@ -51,7 +50,7 @@ match scope with
     | Monomorphic_entry univs -> univs
     | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
   in
-  let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in
+  let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, Decls.IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let r = VarRef ident in
@@ -69,7 +68,7 @@ match scope with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let decl = (Declare.ParameterEntry (None,(typ,univs),inl), IsAssumption kind) in
+  let decl = (Declare.ParameterEntry (None,(typ,univs),inl), Decls.IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -211,7 +210,7 @@ let do_primitive id prim typopt =
                 prim_entry_content = prim;
               }
   in
-  let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
+  let _kn = declare_constant id.CAst.v (PrimitiveEntry entry, Decls.IsPrimitive) in
   Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
 
 let named_of_rel_context l =
@@ -275,10 +274,10 @@ let context ~poly l =
       (* Declare the universe context once *)
       let decl = match b with
       | None ->
-        (Declare.ParameterEntry (None,(t,univs),None), IsAssumption Logical)
+        (Declare.ParameterEntry (None,(t,univs),None), Decls.(IsAssumption Logical))
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
-        (Declare.DefinitionEntry entry, IsAssumption Logical)
+        (Declare.DefinitionEntry entry, Decls.(IsAssumption Logical))
       in
       let cst = Declare.declare_constant id decl in
       let env = Global.env () in
@@ -294,13 +293,13 @@ let context ~poly l =
         if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
       let nstatus = match b with
       | None ->
-        pi3 (declare_assumption false ~scope ~poly ~kind:Context t univs UnivNames.empty_binders [] impl
+        pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
         let _gr = DeclareDef.declare_definition
             ~name:id ~scope:DeclareDef.Discharge
-            ~kind:Definition UnivNames.empty_binders entry [] in
+            ~kind:Decls.Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 57b4aea9e3..028ed39656 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -11,7 +11,6 @@
 open Names
 open Vernacexpr
 open Constrexpr
-open Decl_kinds
 
 (** {6 Parameters/Assumptions} *)
 
@@ -19,7 +18,7 @@ val do_assumptions
   :  program_mode:bool
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:assumption_object_kind
+  -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
   -> bool
@@ -30,7 +29,7 @@ val declare_assumption
   : coercion_flag
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:assumption_object_kind
+  -> kind:Decls.assumption_object_kind
   -> Constr.types
   -> Entries.universes_entry
   -> UnivNames.universe_binders
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 71926a9d23..db0c102e14 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
 open Redexpr
 open Constrexpr
 
@@ -21,7 +20,7 @@ val do_definition
   -> name:Id.t
   -> scope:DeclareDef.locality
   -> poly:bool
-  -> kind:definition_object_kind
+  -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e3428d6afc..cc2f7d9f70 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -20,7 +20,6 @@ open Names
 open Constrexpr
 open Constrexpr_ops
 open Constrintern
-open Decl_kinds
 open Pretyping
 open Evarutil
 open Evarconv
@@ -257,8 +256,8 @@ let interp_fixpoint ~cofix l ntns =
 
 let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
   let fix_kind, cofix, indexes = match indexes with
-    | Some indexes -> Fixpoint, false, indexes
-    | None -> CoFixpoint, true, []
+    | Some indexes -> Decls.Fixpoint, false, indexes
+    | None -> Decls.CoFixpoint, true, []
   in
   let thms =
     List.map3 (fun name t (ctx,impargs,_) ->
@@ -269,7 +268,7 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl
+    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(Decls.DefinitionBody fix_kind) ~udecl
       evd (Some(cofix,indexes,init_tac)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
@@ -278,8 +277,8 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs
 let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let indexes, cofix, fix_kind =
     match indexes with
-    | Some indexes -> indexes, false, Fixpoint
-    | None -> [], true, CoFixpoint
+    | Some indexes -> indexes, false, Decls.Fixpoint
+    | None -> [], true, Decls.CoFixpoint
   in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3947bb1b14..95f8fff520 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -22,7 +22,6 @@ open Nameops
 open Constrexpr
 open Constrexpr_ops
 open Constrintern
-open Decl_kinds
 open Evarutil
 open Context.Rel.Declaration
 open ComFixpoint
@@ -213,7 +212,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
         (*FIXME poly? *)
         let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
         (* FIXME: include locality *)
-        let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
+        let c = Declare.declare_constant recname (DefinitionEntry ce, Decls.(IsDefinition Definition)) in
         let gr = ConstRef c in
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false gr impls
@@ -288,8 +287,8 @@ let do_program_recursive ~scope ~poly fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | DeclareObl.IsFixpoint _ -> Fixpoint
-  | DeclareObl.IsCoFixpoint -> CoFixpoint
+  | DeclareObl.IsFixpoint _ -> Decls.Fixpoint
+  | DeclareObl.IsCoFixpoint -> Decls.CoFixpoint
   in
   Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
 
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index d229973936..7487c99f56 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Decl_kinds
 open Declare
 open Globnames
 open Impargs
@@ -49,10 +48,10 @@ let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
   let gr = match scope with
   | Discharge ->
-      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in
+      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, Decls.IsDefinition kind) in
       VarRef name
   | Global local ->
-      let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in
+      let kn = declare_constant name ~local (DefinitionEntry ce, Decls.IsDefinition kind) in
       let gr = ConstRef kn in
       let () = Declare.declare_univ_binders gr udecl in
       gr
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index cfff89bc34..606cfade46 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
 
 type locality = Discharge | Global of Declare.import_status
 
@@ -43,7 +42,7 @@ end
 val declare_definition
   :  name:Id.t
   -> scope:locality
-  -> kind:definition_object_kind
+  -> kind:Decls.definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
   -> Evd.side_effects Proof_global.proof_entry
@@ -55,7 +54,7 @@ val declare_fix
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> name:Id.t
   -> scope:locality
-  -> kind:definition_object_kind
+  -> kind:Decls.definition_object_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
   -> Evd.side_effects Entries.proof_output
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index cd521255a0..0ab02862f0 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -14,7 +14,6 @@ open Environ
 open Context
 open Constr
 open Vars
-open Decl_kinds
 open Entries
 
 type 'a obligation_body = DefinedObl of 'a | TermObl of constr
@@ -50,7 +49,7 @@ type program_info =
   ; prg_notations : notations
   ; prg_poly : bool
   ; prg_scope : DeclareDef.locality
-  ; prg_kind : definition_object_kind
+  ; prg_kind : Decls.definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
@@ -168,7 +167,7 @@ let declare_obligation prg obl body ty uctx =
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified
-        (Declare.DefinitionEntry ce, IsProof Property)
+        (Declare.DefinitionEntry ce, Decls.(IsProof Property))
     in
     if not opaque then
       add_hint (Locality.make_section_locality None) prg constant;
@@ -423,7 +422,7 @@ let declare_mutual_definition l =
   let fixdecls = (Array.map2 make_annot namevec rvec, arrrec, recvec) in
   let fixnames = first.prg_deps in
   let opaque = first.prg_opaque in
-  let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
+  let kind = if fixkind != IsCoFixpoint then Decls.Fixpoint else Decls.CoFixpoint in
   let indexes, fixdecls =
     match fixkind with
     | IsFixpoint wfl ->
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index fae27e1cb3..7433888cec 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -44,7 +44,7 @@ type program_info =
   ; prg_notations : notations
   ; prg_poly : bool
   ; prg_scope : DeclareDef.locality
-  ; prg_kind : Decl_kinds.definition_object_kind
+  ; prg_kind : Decls.definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 94876d2142..5cffa18511 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -55,7 +55,7 @@ GRAMMAR EXTEND Gram
   ;
   command:
     [ [ IDENT "Goal"; c = lconstr ->
-        { VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) }
+        { VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) }
       | IDENT "Proof" -> { VernacProof (None,None) }
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn }
       | IDENT "Proof"; c = lconstr -> { VernacExactProof c }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74bd552459..2b475f1ef9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -20,7 +20,7 @@ open Impargs
 open Constrexpr
 open Constrexpr_ops
 open Extend
-open Decl_kinds
+open Decls
 open Declaremods
 open Declarations
 open Namegen
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 9559edbea0..26499ce994 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -24,7 +24,6 @@ open Declarations
 open Term
 open Constr
 open Inductive
-open Decl_kinds
 open Indrec
 open Declare
 open Libnames
@@ -114,7 +113,7 @@ let define ~poly id sigma c t =
         proof_entry_inline_code = false;
         proof_entry_feedback = None;
       },
-      Decl_kinds.IsDefinition Scheme) in
+      Decls.(IsDefinition Scheme)) in
   definition_message id;
   kn
 
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e586200ba3..2908481dea 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -22,7 +22,6 @@ open Entries
 open Nameops
 open Globnames
 open Decls
-open Decl_kinds
 open Declare
 open Pretyping
 open Termops
@@ -75,7 +74,7 @@ module Info = struct
     (* This could be improved and the CEphemeron removed *)
     ; other_thms : Recthm.t list
     ; scope : DeclareDef.locality
-    ; kind : Decl_kinds.goal_object_kind
+    ; kind : Decls.goal_object_kind
     }
 
   let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () =
@@ -497,7 +496,7 @@ let finish_proved env sigma idopt po info =
     let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       let const = adjust_guardness_conditions const compute_guard in
-      let k = Kindops.logical_kind_of_goal_kind kind in
+      let k = Decls.logical_kind_of_goal_kind kind in
       let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
       let open DeclareDef in
       let r = match scope with
@@ -543,7 +542,7 @@ let finish_derived ~f ~name ~idopt ~entries =
   (* The opacity of [f_def] is adjusted to be [false], as it
      must. Then [f] is declared in the global environment. *)
   let f_def = { f_def with Proof_global.proof_entry_opaque = false } in
-  let f_def = Declare.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
+  let f_def = Declare.DefinitionEntry f_def , IsDefinition Definition in
   let f_kn = Declare.declare_constant f f_def in
   let f_kn_term = mkConst f_kn in
   (* In the type and body of the proof of [suchthat] there can be
@@ -568,14 +567,13 @@ let finish_derived ~f ~name ~idopt ~entries =
   in
   let lemma_def =
     Declare.DefinitionEntry lemma_def ,
-    Decl_kinds.(IsProof Proposition)
+    Decls.(IsProof Proposition)
   in
   let _ : Names.Constant.t = Declare.declare_constant name lemma_def in
   ()
 
 let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
 
-  let open Decl_kinds in
   let obls = ref 1 in
   let kind = match kind with
     | DefinitionBody d -> IsDefinition d
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index d156954c85..39c074d4ff 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
 
 (** {4 Proofs attached to a constant} *)
 
@@ -68,7 +67,7 @@ module Info : sig
     (** Info for special constants *)
     -> ?scope : DeclareDef.locality
     (** locality  *)
-    -> ?kind:goal_object_kind
+    -> ?kind:Decls.goal_object_kind
     (** Theorem, etc... *)
     -> unit
     -> t
@@ -101,7 +100,7 @@ val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:goal_object_kind
+  -> kind:Decls.goal_object_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
@@ -116,7 +115,7 @@ val start_lemma_com
   :  program_mode:bool
   -> poly:bool
   -> scope:DeclareDef.locality
-  -> kind:goal_object_kind
+  -> kind:Decls.goal_object_kind
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:DeclareDef.Hook.t
   -> Vernacexpr.proof_expr list
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index e82694b740..92adad2299 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Printf
-open Decl_kinds
 
 (**
    - Get types of existentials ;
@@ -398,8 +397,8 @@ let deps_remaining obls deps =
     deps []
 
 
-let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition)
-let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma)
+let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(DefinitionBody Definition))
+let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Decls.(Proof Lemma))
 
 let kind_of_obligation o =
   match o with
@@ -638,7 +637,7 @@ let show_term n =
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
 let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?tactic
+                   ?(implicits=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let info = Id.print name ++ str " has type-checked" in
@@ -658,7 +657,7 @@ let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
-                           ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce)
+                           ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
@@ -690,7 +689,7 @@ let admit_prog prg =
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
             let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified
-              (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
+              (Declare.ParameterEntry (None,(x.obl_type,ctx),None), Decls.(IsAssumption Conjectural))
             in
               assumption_message x.obl_name;
               obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 233739ee46..f97bc784c3 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -50,7 +50,7 @@ val add_definition
   -> ?implicits:Impargs.manual_implicits
   -> poly:bool
   -> ?scope:DeclareDef.locality
-  -> ?kind:Decl_kinds.definition_object_kind
+  -> ?kind:Decls.definition_object_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t
@@ -66,7 +66,7 @@ val add_mutual_definitions
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
   -> ?scope:DeclareDef.locality
-  -> ?kind:Decl_kinds.definition_object_kind
+  -> ?kind:Decls.definition_object_kind
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t -> ?opaque:bool
   -> DeclareObl.notations
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4f053b98ae..78112d9dc4 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -16,7 +16,6 @@ open Util
 open CAst
 
 open Extend
-open Decl_kinds
 open Constrexpr
 open Constrexpr_ops
 open Vernacexpr
@@ -348,18 +347,18 @@ open Pputils
 
   let pr_assumption_token many discharge kind =
     match discharge, kind with
-      | (NoDischarge,Logical) ->
+      | (NoDischarge,Decls.Logical) ->
         keyword (if many then "Axioms" else "Axiom")
-      | (NoDischarge,Definitional) ->
+      | (NoDischarge,Decls.Definitional) ->
         keyword (if many then "Parameters" else "Parameter")
-      | (NoDischarge,Conjectural) -> str"Conjecture"
-      | (DoDischarge,Logical) ->
+      | (NoDischarge,Decls.Conjectural) -> str"Conjecture"
+      | (DoDischarge,Decls.Logical) ->
         keyword (if many then "Hypotheses" else "Hypothesis")
-      | (DoDischarge,Definitional) ->
+      | (DoDischarge,Decls.Definitional) ->
         keyword (if many then "Variables" else "Variable")
-      | (DoDischarge,Conjectural) ->
+      | (DoDischarge,Decls.Conjectural) ->
         anomaly (Pp.str "Don't know how to beautify a local conjecture.")
-      | (_,Context) ->
+      | (_,Decls.Context) ->
         anomaly (Pp.str "Context is used only internally.")
 
   let pr_params pr_c (xl,(c,t)) =
@@ -388,7 +387,16 @@ open Pputils
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
 
-  let pr_thm_token k = keyword (Kindops.string_of_theorem_kind k)
+let string_of_theorem_kind = let open Decls in function
+  | Theorem -> "Theorem"
+  | Lemma -> "Lemma"
+  | Fact -> "Fact"
+  | Remark -> "Remark"
+  | Property -> "Property"
+  | Proposition -> "Proposition"
+  | Corollary -> "Corollary"
+
+  let pr_thm_token k = keyword (string_of_theorem_kind k)
 
   let pr_syntax_modifier = let open Gramlib.Gramext in function
     | SetItemLevel (l,bko,n) ->
@@ -588,6 +596,18 @@ open Pputils
     with Not_found ->
       hov 1 (str "TODO(" ++ str (fst s) ++ spc () ++ prlist_with_sep sep pr_arg cl ++ str ")")
 
+
+let string_of_definition_object_kind = let open Decls in function
+  | Definition -> "Definition"
+  | Example -> "Example"
+  | Coercion -> "Coercion"
+  | SubClass -> "SubClass"
+  | CanonicalStructure -> "Canonical Structure"
+  | Instance -> "Instance"
+  | Let -> "Let"
+  | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
+    CErrors.anomaly (Pp.str "Internal definition kind.")
+
   let pr_vernac_expr v =
     let return = tag_vernac v in
     let env = Global.env () in
@@ -719,7 +739,7 @@ open Pputils
           keyword (
             if Name.is_anonymous (fst id).v
             then "Goal"
-            else Kindops.string_of_definition_object_kind dk)
+            else string_of_definition_object_kind dk)
         in
         let pr_reduce = function
           | None -> mt()
diff --git a/vernac/record.ml b/vernac/record.ml
index cc4f02349d..08239eb544 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -24,7 +24,6 @@ open Declarations
 open Entries
 open Declare
 open Constrintern
-open Decl_kinds
 open Type_errors
 open Constrexpr
 open Constrexpr_ops
@@ -282,7 +281,7 @@ type projection_flags = {
 }
 
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields =
+let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
@@ -352,7 +351,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
                     proof_entry_opaque = false;
                     proof_entry_inline_code = false;
                     proof_entry_feedback = None } in
-                  let k = (Declare.DefinitionEntry entry,IsDefinition kind) in
+                  let k = (Declare.DefinitionEntry entry,Decls.IsDefinition kind) in
                   let kn = declare_constant fid k in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
@@ -402,7 +401,7 @@ let inStruc : Recordops.struc_tuple -> obj =
 let declare_structure_entry o =
   Lib.add_anonymous_leaf (inStruc o)
 
-let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
+let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data =
   let nparams = List.length params in
   let poly, ctx =
     match univs with
@@ -481,7 +480,7 @@ let implicits_of_context ctx =
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
 let declare_class def cum ubinders univs id idbuild paramimpls params arity
-    template fieldimpls fields ?(kind=StructureComponent) coers priorities =
+    template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
     let impls = implicits_of_context params in
@@ -498,7 +497,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       let class_entry = 
         Declare.definition_entry ~types:class_type ~univs class_body in
       let cst = Declare.declare_constant id
-	(DefinitionEntry class_entry, IsDefinition Definition)
+        (DefinitionEntry class_entry, Decls.(IsDefinition Definition))
       in
       let inst, univs = match univs with
         | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
@@ -513,7 +512,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
         it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
       let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
       let proj_cst = Declare.declare_constant proj_name
-        (DefinitionEntry proj_entry, IsDefinition Definition)
+        (DefinitionEntry proj_entry, Decls.(IsDefinition Definition))
       in
       let cref = ConstRef cst in
       Impargs.declare_manual_implicits false cref paramimpls;
@@ -528,7 +527,7 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       let record_data = [id, idbuild, arity, fieldimpls, fields, false,
                          List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls
-        params template ~kind:Method ~name:[|binder_name|] record_data
+        params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
        let coers = List.map2 (fun coe pri -> 
 			      Option.map (fun b -> 
diff --git a/vernac/record.mli b/vernac/record.mli
index d0164572f3..3165448d0c 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -22,7 +22,7 @@ type projection_flags = {
 val declare_projections :
   inductive ->
   Entries.universes_entry ->
-  ?kind:Decl_kinds.definition_object_kind ->
+  ?kind:Decls.definition_object_kind ->
   Id.t ->
   projection_flags list ->
   Impargs.manual_implicits list ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9b9be0209e..cfa25b03bc 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -24,7 +24,6 @@ open Goptions
 open Libnames
 open Globnames
 open Vernacexpr
-open Decl_kinds
 open Constrexpr
 open Redexpr
 open Lemmas
@@ -525,7 +524,7 @@ let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l =
   in
   start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l
 
-let vernac_definition_hook ~poly = function
+let vernac_definition_hook ~poly = let open Decls in function
 | Coercion ->
   Some (Class.add_coercion_hook ~poly)
 | CanonicalStructure ->
@@ -558,7 +557,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+  start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(Decls.DefinitionBody kind) ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
@@ -581,7 +580,7 @@ let vernac_start_proof ~atts kind l =
   let scope = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l
+  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.Proof kind) l
 
 let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index dc5df5904e..eb1bca410a 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -276,11 +276,11 @@ type nonrec vernac_expr =
   | VernacDeclareCustomEntry of string
 
   (* Gallina *)
-  | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
-  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
+  | VernacDefinition of (discharge * Decls.definition_object_kind) * name_decl * definition_expr
+  | VernacStartTheoremProof of Decls.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) *
+  | VernacAssumption of (discharge * Decls.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list