[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.

23 files changed, 93 insertions, 89 deletions

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