[declare] Merge DeclareDef into Declare

The API in `DeclareDef` should become the recommended API in `Declare`.

This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.

This PR originally introduced a dependency cycle due to:

- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`

This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.

There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.

Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...

40 files changed, 480 insertions, 510 deletions

diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index b94b1fc657..e9e866c5fb 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,6 +1,6 @@
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let scope = Declare.Global Declare.ImportDefaultBehavior in
   let kind = Decls.(IsDefinition Definition) in
-  DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
+  Declare.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl
     ~opaque:false ~poly ~types:None ~body sigma
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 07f578d2a8..9366c4250d 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -218,7 +218,7 @@ let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
     Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
   in
   (* uctx was ignored before *)
-  let hook = DeclareDef.Hook.make (hook new_principle_type) in
+  let hook = Declare.Hook.make (hook new_principle_type) in
   (body, typ, univs, hook, sigma)
 
 let change_property_sort evd toSort princ princName =
@@ -318,8 +318,8 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
     let uctx = Evd.evar_universe_context sigma in
     let entry = Declare.definition_entry ~univs ?types body in
     let (_ : Names.GlobRef.t) =
-      DeclareDef.declare_entry ~name:new_princ_name ~hook
-        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      Declare.declare_entry ~name:new_princ_name ~hook
+        ~scope:(Declare.Global Declare.ImportDefaultBehavior)
         ~kind:Decls.(IsProof Theorem)
         ~impargs:[] ~uctx entry
     in
@@ -400,7 +400,7 @@ let register_struct is_rec fixpoint_exprl =
           Pp.(str "Body of Function must be given")
     in
     ComDefinition.do_definition ~name:fname.CAst.v ~poly:false
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.Definition univs binders None body (Some rtype);
     let evd, rev_pconstants =
       List.fold_left
@@ -419,7 +419,7 @@ let register_struct is_rec fixpoint_exprl =
     (None, evd, List.rev rev_pconstants)
   | _ ->
     ComFixpoint.do_fixpoint
-      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false
+      ~scope:(Declare.Global Declare.ImportDefaultBehavior) ~poly:false
       fixpoint_exprl;
     let evd, rev_pconstants =
       List.fold_left
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index ffb9a7e69b..5c82ed38bb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1483,7 +1483,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
     Lemmas.save_lemma_proved ~lemma ~opaque:opacity ~idopt:None
   in
-  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
+  let info = Lemmas.Info.make ~hook:(Declare.Hook.make hook) () in
   let lemma =
     Lemmas.start_lemma ~name:na ~poly:false (* FIXME *) ~info sigma gls_type
   in
@@ -1721,7 +1721,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref Undefined in
   (* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
-  let hook {DeclareDef.Hook.S.uctx; _} =
+  let hook {Declare.Hook.S.uctx; _} =
     let term_ref = Nametab.locate (qualid_of_ident term_id) in
     let f_ref =
       declare_f function_name Decls.(IsProof Lemma) arg_types term_ref
@@ -1767,5 +1767,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls
         functional_ref
         (EConstr.of_constr rec_arg_type)
         relation rec_arg_num term_id using_lemmas (List.length res_vars) evd
-        (DeclareDef.Hook.make hook))
+        (Declare.Hook.make hook))
     ()
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 5baa23b3e9..aef5f645f4 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
+        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 3834b21a14..3b8fb48eb0 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1894,10 +1894,10 @@ let declare_projection name instance_id r =
     in it_mkProd_or_LetIn ccl ctx
   in
   let types = Some (it_mkProd_or_LetIn typ ctx) in
-  let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsDefinition Definition), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let _r : GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
+    Declare.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
   in ()
 
 let build_morphism_signature env sigma m =
@@ -1961,10 +1961,10 @@ let add_morphism_as_parameter atts m n : unit =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let poly = atts.polymorphic in
-  let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kind, opaque, scope = Decls.(IsAssumption Logical), false, Declare.Global Declare.ImportDefaultBehavior in
   let impargs, udecl = [], UState.default_univ_decl in
   let evd, types = build_morphism_signature env evd m in
-  let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+  let evd, pe = Declare.prepare_parameter ~poly ~udecl ~types evd in
   let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
   let cst = GlobRef.ConstRef cst in
   Classes.add_instance
@@ -1981,7 +1981,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let poly = atts.polymorphic in
   let kind = Decls.(IsDefinition Instance) in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
-  let hook { DeclareDef.Hook.S.dref; _ } = dref |> function
+  let hook { Declare.Hook.S.dref; _ } = dref |> function
     | GlobRef.ConstRef cst ->
       Classes.add_instance (Classes.mk_instance
                       (PropGlobal.proper_class env evd) Hints.empty_hint_info
@@ -1989,7 +1989,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (GlobRef.ConstRef cst)
     | _ -> assert false
   in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
diff --git a/vernac/classes.ml b/vernac/classes.ml
index eb735b7cdf..55af2e1a7d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -313,8 +313,8 @@ let instance_hook info global ?hook cst =
 
 let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
-  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs
+  let scope = Declare.Global Declare.ImportDefaultBehavior in
+  let kn = Declare.declare_definition ~name ~kind ~scope ~impargs
       ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
   instance_hook info global ?hook kn
 
@@ -325,7 +325,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in
+  let sigma, entry = Declare.prepare_parameter ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
@@ -334,7 +334,7 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   instance_hook pri global cst
 
 let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype =
-  let hook { DeclareDef.Hook.S.scope; dref; _ } =
+  let hook { Declare.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
     let pri = intern_info pri in
     let env = Global.env () in
@@ -342,9 +342,9 @@ let declare_instance_program env sigma ~global ~poly name pri impargs udecl term
     declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst)
   in
   let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
-  let hook = DeclareDef.Hook.make hook in
+  let hook = Declare.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
-  let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
+  let scope, kind = Declare.Global Declare.ImportDefaultBehavior, Decls.Instance in
   let _ : DeclareObl.progress =
     Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
@@ -357,7 +357,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs udecl id
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
-  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
+  let hook = Declare.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~kind () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index f410cddfef..1b6deb3b28 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
     Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
     when said type is not a registered type class. *)
 
-val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> Vernacexpr.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
 val new_instance_interactive
@@ -34,7 +34,7 @@ val new_instance_interactive
   -> ?generalize:bool
   -> ?tac:unit Proofview.tactic
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> (bool * constr_expr) option
   -> Id.t * Lemmas.t
 
@@ -47,7 +47,7 @@ val new_instance
   -> (bool * constr_expr)
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> Id.t
 
 val new_instance_program
@@ -59,7 +59,7 @@ val new_instance_program
   -> (bool * constr_expr) option
   -> ?generalize:bool
   -> ?hook:(GlobRef.t -> unit)
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> Id.t
 
 val declare_new_instance
@@ -69,7 +69,7 @@ val declare_new_instance
   -> ident_decl
   -> local_binder_expr list
   -> constr_expr
-  -> ComHints.hint_info_expr
+  -> Vernacexpr.hint_info_expr
   -> unit
 
 (** {6 Low level interface used by Add Morphism, do not use } *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 776ffd6b9f..023d76ce3b 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -87,8 +87,7 @@ let context_set_of_entry = function
   | Monomorphic_entry uctx -> uctx
 
 let declare_assumptions ~poly ~scope ~kind univs nl l =
-  let open DeclareDef in
-  let () = match scope with
+  let () = let open Declare in match scope with
     | Discharge ->
       (* declare universes separately for variables *)
       DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
@@ -100,10 +99,10 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
       let univs,subst' =
         List.fold_left_map (fun univs id ->
             let refu = match scope with
-              | Discharge ->
+              | Declare.Discharge ->
                 declare_variable is_coe ~kind typ imps Glob_term.Explicit id;
                 GlobRef.VarRef id.CAst.v, Univ.Instance.empty
-              | Global local ->
+              | Declare.Global local ->
                 declare_axiom is_coe ~local ~poly ~kind typ univs imps nl id
             in
             next_univs univs, (id.CAst.v, Constr.mkRef refu))
@@ -130,7 +129,7 @@ let process_assumptions_udecls ~scope l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let open DeclareDef in
+  let open Declare in
   let () = match scope, udecl with
     | Discharge, Some _ ->
       let loc = first_id.CAst.loc in
@@ -208,7 +207,7 @@ let context_insection sigma ~poly ctx =
         let uctx = Evd.evar_universe_context sigma in
         let kind = Decls.(IsDefinition Definition) in
         let _ : GlobRef.t =
-          DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge
+          Declare.declare_entry ~name ~scope:Declare.Discharge
             ~kind ~impargs:[] ~uctx entry
         in
         ()
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 4b953c8869..989015a9f3 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,7 +17,7 @@ open Constrexpr
 val do_assumptions
   :  program_mode:bool
   -> poly:bool
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> kind:Decls.assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
diff --git a/vernac/comCoercion.ml b/vernac/comCoercion.ml
index 4a8e217fc1..d6be02245c 100644
--- a/vernac/comCoercion.ml
+++ b/vernac/comCoercion.ml
@@ -352,8 +352,8 @@ let try_add_new_identity_coercion id ~local ~poly ~source ~target =
 let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
-let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } =
-  let open DeclareDef in
+let add_coercion_hook poly { Declare.Hook.S.scope; dref; _ } =
+  let open Declare in
   let local = match scope with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -363,10 +363,10 @@ let add_coercion_hook poly { DeclareDef.Hook.S.scope; dref; _ } =
   let msg = Nametab.pr_global_env Id.Set.empty dref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly)
+let add_coercion_hook ~poly = Declare.Hook.make (add_coercion_hook poly)
 
-let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } =
-  let open DeclareDef in
+let add_subclass_hook ~poly { Declare.Hook.S.scope; dref; _ } =
+  let open Declare in
   let stre = match scope with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
@@ -375,4 +375,4 @@ let add_subclass_hook ~poly { DeclareDef.Hook.S.scope; dref; _ } =
   let cl = class_of_global dref in
   try_add_new_coercion_subclass cl ~local:stre ~poly
 
-let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly)
+let add_subclass_hook ~poly = Declare.Hook.make (add_subclass_hook ~poly)
diff --git a/vernac/comCoercion.mli b/vernac/comCoercion.mli
index 3b44bdaf8a..dee693232f 100644
--- a/vernac/comCoercion.mli
+++ b/vernac/comCoercion.mli
@@ -46,8 +46,8 @@ val try_add_new_identity_coercion
   -> local:bool
   -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : poly:bool -> DeclareDef.Hook.t
+val add_coercion_hook : poly:bool -> Declare.Hook.t
 
-val add_subclass_hook : poly:bool -> DeclareDef.Hook.t
+val add_subclass_hook : poly:bool -> Declare.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 66d5a4f7f5..95f3955309 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -117,7 +117,7 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
   in
   let kind = Decls.IsDefinition kind in
   let _ : Names.GlobRef.t =
-    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs
+    Declare.declare_definition ~name ~scope ~kind ?hook ~impargs
       ~opaque:false ~poly evd ~udecl ~types ~body
   in ()
 
@@ -126,7 +126,7 @@ let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c c
   let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let term, ty, uctx, obls = Declare.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
   let _ : DeclareObl.progress =
     Obligations.add_definition
       ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 337da22018..2e8fe16252 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -15,9 +15,9 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  ?hook:DeclareDef.Hook.t
+  :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
@@ -28,9 +28,9 @@ val do_definition
   -> unit
 
 val do_definition_program
-  :  ?hook:DeclareDef.Hook.t
+  :  ?hook:Declare.Hook.t
   -> name:Id.t
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> poly:bool
   -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index e4fa212a23..626f913b3f 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -248,7 +248,7 @@ let build_recthms ~indexes fixnames fixtypes fiximps =
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { DeclareDef.Recthm.name
+        { Declare.Recthm.name
         ; typ
         ; args = List.map Context.Rel.Declaration.get_name ctx
         ; impargs})
@@ -275,7 +275,7 @@ let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixt
   let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
   let fix_kind = Decls.IsDefinition fix_kind in
   let _ : GlobRef.t list =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
+    Declare.declare_mutually_recursive ~scope ~opaque:false ~kind:fix_kind ~poly ~uctx
       ~possible_indexes:indexes ~restrict_ucontext:true ~udecl ~ntns ~rec_declaration
       fixitems
   in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index a19b96f0f3..bdb1ac19d4 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -16,16 +16,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> Lemmas.t
 
 val do_fixpoint :
-  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint_interactive :
-  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> Lemmas.t
 
 val do_cofixpoint :
-  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
index 5a48e9c16c..2fd6fe2b29 100644
--- a/vernac/comHints.ml
+++ b/vernac/comHints.ml
@@ -13,23 +13,6 @@ open Util
 (** (Partial) implementation of the [Hint] command; some more
    functionality still lives in tactics/hints.ml *)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
-
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.qualid list
-  | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
-  | HintsMode of Libnames.qualid * Hints.hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of
-      int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 let project_hint ~poly pri l2r r =
   let open EConstr in
   let open Coqlib in
@@ -108,6 +91,7 @@ let interp_hints ~poly h =
   let fr r = Tacred.evaluable_of_global_reference env (fref r) in
   let fi c =
     let open Hints in
+    let open Vernacexpr in
     match c with
     | HintsReference c ->
       let gr = Smartlocate.global_with_alias c in
@@ -126,15 +110,14 @@ let interp_hints ~poly h =
     in
     (info, poly, b, path, gr)
   in
-  let ft =
-    let open Hints in
-    function
+  let open Hints in
+  let open Vernacexpr in
+  let ft = function
     | HintsVariables -> HintsVariables
     | HintsConstants -> HintsConstants
     | HintsReferences lhints -> HintsReferences (List.map fr lhints)
   in
   let fp = Constrintern.intern_constr_pattern (Global.env ()) in
-  let open Hints in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsResolveIFF (l2r, lc, n) ->
diff --git a/vernac/comHints.mli b/vernac/comHints.mli
index 77fbef5387..20894eecf1 100644
--- a/vernac/comHints.mli
+++ b/vernac/comHints.mli
@@ -8,22 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Typeclasses
-
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * Libnames.qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of Libnames.qualid list
-  | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
-  | HintsMode of Libnames.qualid * Hints.hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
-val interp_hints : poly:bool -> hints_expr -> Hints.hints_entry
+val interp_hints : poly:bool -> Vernacexpr.hints_expr -> Hints.hints_entry
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index bf38088f71..4e9e24b119 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -230,7 +230,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       let name = add_suffix recname "_func" in
       (* XXX: Mutating the evar_map in the hook! *)
       (* XXX: Likely the sigma is out of date when the hook is called .... *)
-      let hook sigma { DeclareDef.Hook.S.dref; _ } =
+      let hook sigma { Declare.Hook.S.dref; _ } =
         let sigma, h_body = Evarutil.new_global sigma dref in
         let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
         let ty = it_mkProd_or_LetIn top_arity binders_rel in
@@ -248,13 +248,13 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       hook, name, typ
     else
       let typ = it_mkProd_or_LetIn top_arity binders_rel in
-      let hook sigma { DeclareDef.Hook.S.dref; _ } =
+      let hook sigma { Declare.Hook.S.dref; _ } =
         if Impargs.is_implicit_args () || not (List.is_empty impls) then
           Impargs.declare_manual_implicits false dref impls
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = DeclareDef.Hook.make (hook sigma) in
+  let hook = Declare.Hook.make (hook sigma) in
   RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     RetrieveObl.retrieve_obligations env recname sigma 0 def typ
@@ -290,7 +290,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
     let evars, _, def, typ =
       RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars)
+    ({ Declare.Recthm.name; typ; impargs; args = [] }, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 6851c9f69e..8b1fa6c202 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -14,8 +14,8 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  scope:DeclareDef.locality -> poly:bool -> fixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> fixpoint_expr list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  scope:DeclareDef.locality -> poly:bool -> cofixpoint_expr list -> unit
+  scope:Declare.locality -> poly:bool -> cofixpoint_expr list -> unit
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 458002f03c..1d39963621 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -16,7 +16,7 @@ open Names
 open Safe_typing
 module NamedDecl = Context.Named.Declaration
 
-type opacity_flag = Opaque | Transparent
+type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
 
 type t =
   { endline_tactic : Genarg.glob_generic_argument option
@@ -120,17 +120,6 @@ let get_open_goals ps =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) stack) +
   List.length shelf
 
-(* object_kind , id *)
-exception AlreadyDeclared of (string option * Id.t)
-
-let _ = CErrors.register_handler (function
-    | AlreadyDeclared (kind, id) ->
-      Some
-        (seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
-             ; Id.print id; str " already exists."])
-    | _ ->
-      None)
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** Declaration of constants and parameters *)
@@ -267,7 +256,7 @@ type constant_obj = {
 
 let load_constant i ((sp,kn), obj) =
   if Nametab.exists_cci sp then
-    raise (AlreadyDeclared (None, Libnames.basename sp));
+    raise (DeclareUniv.AlreadyDeclared (None, Libnames.basename sp));
   let con = Global.constant_of_delta_kn kn in
   Nametab.push (Nametab.Until i) sp (GlobRef.ConstRef con);
   Dumpglob.add_constant_kind con obj.cst_kind
@@ -287,7 +276,7 @@ let exists_name id =
 
 let check_exists id =
   if exists_name id then
-    raise (AlreadyDeclared (None, id))
+    raise (DeclareUniv.AlreadyDeclared (None, id))
 
 let cache_constant ((sp,kn), obj) =
   (* Invariant: the constant must exist in the logical environment *)
@@ -548,7 +537,7 @@ let inVariable v = Libobject.Dyn.Easy.inj v objVariable
 let declare_variable ~name ~kind d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
-    raise (AlreadyDeclared (None, name));
+    raise (DeclareUniv.AlreadyDeclared (None, name));
 
   let impl,opaque = match d with (* Fails if not well-typed *)
     | SectionLocalAssum {typ;impl} ->
@@ -886,3 +875,181 @@ let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
 let _ = Abstract.declare_abstract := declare_abstract
 
 let declare_universe_context = DeclareUctx.declare_universe_context
+
+type locality = Discharge | Global of import_status
+
+(* Hooks naturally belong here as they apply to both definitions and lemmas *)
+module Hook = struct
+  module S = struct
+    type t =
+      { uctx : UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      ; obls : (Names.Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      ; scope : locality
+      (**  [locality]: Locality of the original declaration *)
+      ; dref : Names.GlobRef.t
+      (** [ref]: identifier of the original declaration *)
+      }
+  end
+
+  type t = (S.t -> unit) CEphemeron.key
+
+  let make hook = CEphemeron.create hook
+
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+
+end
+
+(* Locality stuff *)
+let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
+  let should_suggest = entry.proof_entry_opaque &&
+                       Option.is_empty entry.proof_entry_secctx in
+  let ubind = UState.universe_binders uctx in
+  let dref = match scope with
+  | Discharge ->
+    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
+    if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
+    Names.GlobRef.VarRef name
+  | Global local ->
+    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
+    let gr = Names.GlobRef.ConstRef kn in
+    if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
+    let () = DeclareUniv.declare_univ_binders gr ubind in
+    gr
+  in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
+  let () = definition_message name in
+  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
+  dref
+
+let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
+  match possible_indexes with
+  | Some possible_indexes ->
+    let env = Global.env() in
+    let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
+    let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
+    vars, fixdecls, Some indexes
+  | None ->
+    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in
+    let vars = Vars.universes_of_constr (List.hd fixdecls) in
+    vars, fixdecls, None
+
+module Recthm = struct
+  type t =
+    { name : Names.Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Names.Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
+  let vars, fixdecls, indexes =
+    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
+  let uctx, univs =
+    (* XXX: Obligations don't do this, this seems like a bug? *)
+    if restrict_ucontext
+    then
+      let uctx = UState.restrict uctx vars in
+      let univs = UState.check_univ_decl ~poly uctx udecl in
+      uctx, univs
+    else
+      let univs = UState.univ_entry ~poly uctx in
+      uctx, univs
+  in
+  let csts = CList.map2
+      (fun Recthm.{ name; typ; impargs } body ->
+         let entry = definition_entry ~opaque ~types:typ ~univs body in
+         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
+      fixitems fixdecls
+  in
+  let isfix = Option.has_some possible_indexes in
+  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
+  recursive_message isfix indexes fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  csts
+
+let warn_let_as_axiom =
+  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+    Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
+                  spc () ++ strbrk "declared as an axiom.")
+
+let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
+  let local = match scope with
+    | Discharge -> warn_let_as_axiom name; ImportNeedQualified
+    | Global local -> local
+  in
+  let kind = Decls.(IsAssumption Conjectural) in
+  let decl = ParameterEntry pe in
+  let kn = declare_constant ~name ~local ~kind decl in
+  let dref = Names.GlobRef.ConstRef kn in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
+  let () = assumption_message name in
+  let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
+  let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
+  dref
+
+let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+  try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+  with exn ->
+    let exn = Exninfo.capture exn in
+    let exn = Option.cata (fun fix -> fix exn) exn fix_exn in
+    Exninfo.iraise exn
+
+(* Preparing proof entries *)
+
+let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let uctx = Evd.evar_universe_context sigma in
+  entry, uctx
+
+let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+    ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+  let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+  declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
+
+let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let ce = definition_entry ?opaque ?inline ?types ~univs body in
+  let env = Global.env () in
+  let (c,ctx), sideff = Future.force ce.proof_entry_body in
+  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
+  assert(Univ.ContextSet.is_empty ctx);
+  RetrieveObl.check_evars env sigma;
+  let c = EConstr.of_constr c in
+  let typ = match ce.proof_entry_type with
+    | Some t -> EConstr.of_constr t
+    | None -> Retyping.get_type_of env sigma c
+  in
+  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let uctx = Evd.evar_universe_context sigma in
+  c, cty, uctx, obls
+
+let prepare_parameter ~poly ~udecl ~types sigma =
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
+      sigma (fun nf -> nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  sigma, (None(*proof using*), (typ, univs), None(*inline*))
+
+(* Compat: will remove *)
+exception AlreadyDeclared = DeclareUniv.AlreadyDeclared
diff --git a/vernac/declare.mli b/vernac/declare.mli
index df81291e7e..340c035d1d 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -69,7 +69,7 @@ module Proof : sig
 
 end
 
-type opacity_flag = Opaque | Transparent
+type opacity_flag = Vernacexpr.opacity_flag = Opaque | Transparent
 
 (** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
    name [name] with goals [goals] (a list of pairs of environment and
@@ -194,14 +194,9 @@ val inline_private_constants
 val definition_message : Id.t -> unit
 val assumption_message : Id.t -> unit
 val fixpoint_message : int array option -> Id.t list -> unit
-val recursive_message : bool (** true = fixpoint *) ->
-  int array option -> Id.t list -> unit
 
 val check_exists : Id.t -> unit
 
-(* Used outside this module only in indschemes *)
-exception AlreadyDeclared of (string option * Id.t)
-
 (** {6 For legacy support, do not use}  *)
 
 module Internal : sig
@@ -278,3 +273,127 @@ val build_constant_by_tactic :
 
 val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 [@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
+
+type locality = Discharge | Global of import_status
+
+(** Declaration hooks *)
+module Hook : sig
+  type t
+
+  (** Hooks allow users of the API to perform arbitrary actions at
+     proof/definition saving time. For example, to register a constant
+     as a Coercion, perform some cleanup, update the search database,
+     etc...  *)
+  module S : sig
+    type t =
+      { uctx : UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      ; obls : (Id.t * Constr.t) list
+      (** [(n1,t1),...(nm,tm)]: association list between obligation
+          name and the corresponding defined term (might be a constant,
+          but also an arbitrary term in the Expand case of obligations) *)
+      ; scope : locality
+      (** [scope]: Locality of the original declaration *)
+      ; dref : GlobRef.t
+      (** [dref]: identifier of the original declaration *)
+      }
+  end
+
+  val make : (S.t -> unit) -> t
+  val call : ?hook:t -> S.t -> unit
+end
+
+(** Declare an interactively-defined constant *)
+val declare_entry
+  :  name:Id.t
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Evd.side_effects proof_entry
+  -> GlobRef.t
+
+(** Declares a non-interactive constant; [body] and [types] will be
+   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
+   be handled properly, including minimization and restriction. Note
+   that [sigma] is checked for unresolved evars, thus you should be
+   careful not to submit open terms or evar maps with stale,
+   unresolved existentials *)
+val declare_definition
+  :  name:Id.t
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> opaque:bool
+  -> impargs:Impargs.manual_implicits
+  -> udecl:UState.universe_decl
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
+  -> poly:bool
+  -> ?inline:bool
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> Evd.evar_map
+  -> GlobRef.t
+
+val declare_assumption
+  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> name:Id.t
+  -> scope:locality
+  -> hook:Hook.t option
+  -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
+  -> Entries.parameter_entry
+  -> GlobRef.t
+
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : Constr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+val declare_mutually_recursive
+  : opaque:bool
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> poly:bool
+  -> uctx:UState.t
+  -> udecl:UState.universe_decl
+  -> ntns:Vernacexpr.decl_notation list
+  -> rec_declaration:Constr.rec_declaration
+  -> possible_indexes:int list list option
+  -> ?restrict_ucontext:bool
+  (** XXX: restrict_ucontext should be always true, this seems like a
+     bug in obligations, so this parameter should go away *)
+  -> Recthm.t list
+  -> Names.GlobRef.t list
+
+val prepare_obligation
+  :  ?opaque:bool
+  -> ?inline:bool
+  -> name:Id.t
+  -> poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> Evd.evar_map
+  -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
+
+val prepare_parameter
+  : poly:bool
+  -> udecl:UState.universe_decl
+  -> types:EConstr.types
+  -> Evd.evar_map
+  -> Evd.evar_map * Entries.parameter_entry
+
+(* Compat: will remove *)
+exception AlreadyDeclared of (string option * Names.Id.t)
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 90d88b95a2..83bb1dae71 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -1,186 +1,9 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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 Declare
-
-type locality = Discharge | Global of Declare.import_status
-
-(* Hooks naturally belong here as they apply to both definitions and lemmas *)
-module Hook = struct
-  module S = struct
-    type t =
-      { uctx : UState.t
-      (** [ustate]: universe constraints obtained when the term was closed *)
-      ; obls : (Names.Id.t * Constr.t) list
-      (** [(n1,t1),...(nm,tm)]: association list between obligation
-          name and the corresponding defined term (might be a constant,
-          but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : locality
-      (**  [locality]: Locality of the original declaration *)
-      ; dref : Names.GlobRef.t
-      (** [ref]: identifier of the original declaration *)
-      }
-  end
-
-  type t = (S.t -> unit) CEphemeron.key
-
-  let make hook = CEphemeron.create hook
-
-  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
-
-end
-
-(* Locality stuff *)
-let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
-  let should_suggest = entry.Declare.proof_entry_opaque &&
-                       Option.is_empty entry.Declare.proof_entry_secctx in
-  let ubind = UState.universe_binders uctx in
-  let dref = match scope with
-  | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
-    if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
-    Names.GlobRef.VarRef name
-  | Global local ->
-    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
-    let gr = Names.GlobRef.ConstRef kn in
-    if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
-    let () = DeclareUniv.declare_univ_binders gr ubind in
-    gr
-  in
-  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
-  let () = definition_message name in
-  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
-  dref
-
-let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
-  match possible_indexes with
-  | Some possible_indexes ->
-    let env = Global.env() in
-    let indexes = Pretyping.search_guard env possible_indexes rec_declaration in
-    let vars = Vars.universes_of_constr (Constr.mkFix ((indexes,0),rec_declaration)) in
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkFix ((indexes,i),rec_declaration)) 0 fixitems in
-    vars, fixdecls, Some indexes
-  | None ->
-    let fixdecls = CList.map_i (fun i _ -> Constr.mkCoFix (i,rec_declaration)) 0 fixitems in
-    let vars = Vars.universes_of_constr (List.hd fixdecls) in
-    vars, fixdecls, None
-
-module Recthm = struct
-  type t =
-    { name : Names.Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Names.Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
-let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
-  let vars, fixdecls, indexes =
-    mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
-  let uctx, univs =
-    (* XXX: Obligations don't do this, this seems like a bug? *)
-    if restrict_ucontext
-    then
-      let uctx = UState.restrict uctx vars in
-      let univs = UState.check_univ_decl ~poly uctx udecl in
-      uctx, univs
-    else
-      let univs = UState.univ_entry ~poly uctx in
-      uctx, univs
-  in
-  let csts = CList.map2
-      (fun Recthm.{ name; typ; impargs } body ->
-         let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
-         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
-      fixitems fixdecls
-  in
-  let isfix = Option.has_some possible_indexes in
-  let fixnames = List.map (fun { Recthm.name } -> name) fixitems in
-  Declare.recursive_message isfix indexes fixnames;
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
-  csts
-
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-    Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
-                  spc () ++ strbrk "declared as an axiom.")
-
-let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
-  let local = match scope with
-    | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
-    | Global local -> local
-  in
-  let kind = Decls.(IsAssumption Conjectural) in
-  let decl = Declare.ParameterEntry pe in
-  let kn = Declare.declare_constant ~name ~local ~kind decl in
-  let dref = Names.GlobRef.ConstRef kn in
-  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
-  let () = Declare.assumption_message name in
-  let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
-  let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
-  dref
-
-let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
-  try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
-  with exn ->
-    let exn = Exninfo.capture exn in
-    let exn = Option.cata (fun fix -> fix exn) exn fix_exn in
-    Exninfo.iraise exn
-
-(* Preparing proof entries *)
-
-let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
-  let env = Global.env () in
-  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
-      sigma (fun nf -> nf body, Option.map nf types)
-  in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
-  let uctx = Evd.evar_universe_context sigma in
-  entry, uctx
-
-let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
-    ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
-  let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
-  declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
-
-let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
-      sigma (fun nf -> nf body, Option.map nf types)
-  in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
-  let ce = definition_entry ?opaque ?inline ?types ~univs body in
-  let env = Global.env () in
-  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-  assert(Safe_typing.is_empty_private_constants sideff.Evd.seff_private);
-  assert(Univ.ContextSet.is_empty ctx);
-  RetrieveObl.check_evars env sigma;
-  let c = EConstr.of_constr c in
-  let typ = match ce.Declare.proof_entry_type with
-    | Some t -> EConstr.of_constr t
-    | None -> Retyping.get_type_of env sigma c
-  in
-  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
-  let uctx = Evd.evar_universe_context sigma in
-  c, cty, uctx, obls
-
-let prepare_parameter ~poly ~udecl ~types sigma =
-  let env = Global.env () in
-  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
-  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
-      sigma (fun nf -> nf types)
-  in
-  let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, (None(*proof using*), (typ, univs), None(*inline*))
+type locality = Declare.locality =
+  | Discharge [@ocaml.deprecated "Use [Declare.Discharge]"]
+  | Global of Declare.import_status [@ocaml.deprecated "Use [Declare.Global]"]
+[@@ocaml.deprecated "Use [Declare.locality]"]
+
+let declare_definition = Declare.declare_definition
+[@@ocaml.deprecated "Use [Declare.declare_definition]"]
+module Hook = Declare.Hook
+[@@ocaml.deprecated "Use [Declare.Hook]"]
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
deleted file mode 100644
index 3bc1e25f19..0000000000
--- a/vernac/declareDef.mli
+++ /dev/null
@@ -1,132 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \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 Names
-
-type locality = Discharge | Global of Declare.import_status
-
-(** Declaration hooks *)
-module Hook : sig
-  type t
-
-  (** Hooks allow users of the API to perform arbitrary actions at
-     proof/definition saving time. For example, to register a constant
-     as a Coercion, perform some cleanup, update the search database,
-     etc...  *)
-  module S : sig
-    type t =
-      { uctx : UState.t
-      (** [ustate]: universe constraints obtained when the term was closed *)
-      ; obls : (Id.t * Constr.t) list
-      (** [(n1,t1),...(nm,tm)]: association list between obligation
-          name and the corresponding defined term (might be a constant,
-          but also an arbitrary term in the Expand case of obligations) *)
-      ; scope : locality
-      (** [scope]: Locality of the original declaration *)
-      ; dref : GlobRef.t
-      (** [dref]: identifier of the original declaration *)
-      }
-  end
-
-  val make : (S.t -> unit) -> t
-  val call : ?hook:t -> S.t -> unit
-end
-
-(** Declare an interactively-defined constant *)
-val declare_entry
-  :  name:Id.t
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> ?hook:Hook.t
-  -> ?obls:(Id.t * Constr.t) list
-  -> impargs:Impargs.manual_implicits
-  -> uctx:UState.t
-  -> Evd.side_effects Declare.proof_entry
-  -> GlobRef.t
-
-(** Declares a non-interactive constant; [body] and [types] will be
-   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
-   be handled properly, including minimization and restriction. Note
-   that [sigma] is checked for unresolved evars, thus you should be
-   careful not to submit open terms or evar maps with stale,
-   unresolved existentials *)
-val declare_definition
-  :  name:Id.t
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> opaque:bool
-  -> impargs:Impargs.manual_implicits
-  -> udecl:UState.universe_decl
-  -> ?hook:Hook.t
-  -> ?obls:(Id.t * Constr.t) list
-  -> poly:bool
-  -> ?inline:bool
-  -> types:EConstr.t option
-  -> body:EConstr.t
-  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-  -> Evd.evar_map
-  -> GlobRef.t
-
-val declare_assumption
-  :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
-  -> name:Id.t
-  -> scope:locality
-  -> hook:Hook.t option
-  -> impargs:Impargs.manual_implicits
-  -> uctx:UState.t
-  -> Entries.parameter_entry
-  -> GlobRef.t
-
-module Recthm : sig
-  type t =
-    { name : Id.t
-    (** Name of theorem *)
-    ; typ : Constr.t
-    (** Type of theorem  *)
-    ; args : Name.t list
-    (** Names to pre-introduce  *)
-    ; impargs : Impargs.manual_implicits
-    (** Explicitily declared implicit arguments  *)
-    }
-end
-
-val declare_mutually_recursive
-  : opaque:bool
-  -> scope:locality
-  -> kind:Decls.logical_kind
-  -> poly:bool
-  -> uctx:UState.t
-  -> udecl:UState.universe_decl
-  -> ntns:Vernacexpr.decl_notation list
-  -> rec_declaration:Constr.rec_declaration
-  -> possible_indexes:int list list option
-  -> ?restrict_ucontext:bool
-  (** XXX: restrict_ucontext should be always true, this seems like a
-     bug in obligations, so this parameter should go away *)
-  -> Recthm.t list
-  -> Names.GlobRef.t list
-
-val prepare_obligation
-  :  ?opaque:bool
-  -> ?inline:bool
-  -> name:Id.t
-  -> poly:bool
-  -> udecl:UState.universe_decl
-  -> types:EConstr.t option
-  -> body:EConstr.t
-  -> Evd.evar_map
-  -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
-
-val prepare_parameter
-  : poly:bool
-  -> udecl:UState.universe_decl
-  -> types:EConstr.types
-  -> Evd.evar_map
-  -> Evd.evar_map * Entries.parameter_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index bba3687256..ab11472dec 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -55,10 +55,10 @@ module ProgramDecl = struct
     ; prg_implicits : Impargs.manual_implicits
     ; prg_notations : Vernacexpr.decl_notation list
     ; prg_poly : bool
-    ; prg_scope : DeclareDef.locality
+    ; prg_scope : Declare.locality
     ; prg_kind : Decls.definition_object_kind
     ; prg_reduce : constr -> constr
-    ; prg_hook : DeclareDef.Hook.t option
+    ; prg_hook : Declare.Hook.t option
     ; prg_opaque : bool
     }
 
@@ -373,7 +373,7 @@ let declare_definition prg =
   (* XXX: This is doing normalization twice *)
   let () = progmap_remove prg in
   let kn =
-    DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
+    Declare.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
       ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
   in
   kn
@@ -426,7 +426,7 @@ let declare_mutual_definition l =
   let fixdefs, fixrs, fixtypes, fixitems =
     List.fold_right2 (fun (d,r,typ,impargs) name (a1,a2,a3,a4) ->
         d :: a1, r :: a2, typ :: a3,
-        DeclareDef.Recthm.{ name; typ; impargs; args = [] } :: a4
+        Declare.Recthm.{ name; typ; impargs; args = [] } :: a4
       ) defs first.prg_deps ([],[],[],[])
   in
   let fixkind = Option.get first.prg_fixkind in
@@ -446,13 +446,13 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let udecl = UState.default_univ_decl in
   let kns =
-    DeclareDef.declare_mutually_recursive ~scope ~opaque ~kind
+    Declare.declare_mutually_recursive ~scope ~opaque ~kind
       ~udecl ~ntns ~uctx:first.prg_ctx ~rec_declaration ~possible_indexes ~poly
       ~restrict_ucontext:false fixitems
   in
   (* Only for the first constant *)
   let dref = List.hd kns in
-  DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref });
+  Declare.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
   dref
 
@@ -556,7 +556,7 @@ let obligation_terminator entries uctx { name; num; auto } =
 
 (* Similar to the terminator but for interactive paths, as the
    terminator is only called in interactive proof mode *)
-let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ } =
+let obligation_hook prg obl num auto { Declare.Hook.S.uctx = ctx'; dref; _ } =
   let { obls; remaining=rem } = prg.prg_obligations in
   let cst = match dref with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index 16c0413caf..03f0a57bcb 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -52,22 +52,22 @@ module ProgramDecl : sig
     ; prg_implicits : Impargs.manual_implicits
     ; prg_notations : Vernacexpr.decl_notation list
     ; prg_poly : bool
-    ; prg_scope : DeclareDef.locality
+    ; prg_scope : Declare.locality
     ; prg_kind : Decls.definition_object_kind
     ; prg_reduce : constr -> constr
-    ; prg_hook : DeclareDef.Hook.t option
+    ; prg_hook : Declare.Hook.t option
     ; prg_opaque : bool
     }
 
   val make :
     ?opaque:bool
-    -> ?hook:DeclareDef.Hook.t
+    -> ?hook:Declare.Hook.t
     -> Names.Id.t
     -> udecl:UState.universe_decl
     -> uctx:UState.t
     -> impargs:Impargs.manual_implicits
     -> poly:bool
-    -> scope:DeclareDef.locality
+    -> scope:Declare.locality
     -> kind:Decls.definition_object_kind
     -> Constr.constr option
     -> Constr.types
@@ -126,7 +126,7 @@ val obligation_hook
   -> Obligation.t
   -> Int.t
   -> (Names.Id.t option -> Int.Set.t -> 'a option -> 'b)
-  -> DeclareDef.Hook.S.t
+  -> Declare.Hook.S.t
   -> unit
 (** [obligation_hook] part 2 of saving an obligation, non-interactive mode *)
 
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 89f3503f4d..1705915e70 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -10,6 +10,17 @@
 
 open Names
 
+(* object_kind , id *)
+exception AlreadyDeclared of (string option * Id.t)
+
+let _ = CErrors.register_handler (function
+    | AlreadyDeclared (kind, id) ->
+      Some
+        Pp.(seq [ Pp.pr_opt_no_spc (fun s -> str s ++ spc ()) kind
+                ; Id.print id; str " already exists."])
+    | _ ->
+      None)
+
 type universe_source =
   | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
   | QualifiedUniv of Id.t (* global universe introduced by some global value *)
@@ -19,7 +30,7 @@ type universe_name_decl = universe_source * (Id.t * Univ.Level.UGlobal.t) list
 
 let check_exists_universe sp =
   if Nametab.exists_universe sp then
-    raise (Declare.AlreadyDeclared (Some "Universe", Libnames.basename sp))
+    raise (AlreadyDeclared (Some "Universe", Libnames.basename sp))
   else ()
 
 let qualify_univ i dp src id =
diff --git a/vernac/declareUniv.mli b/vernac/declareUniv.mli
index 51f3f5e0fb..e4d1d5dc65 100644
--- a/vernac/declareUniv.mli
+++ b/vernac/declareUniv.mli
@@ -10,6 +10,9 @@
 
 open Names
 
+(* object_kind , id *)
+exception AlreadyDeclared of (string option * Id.t)
+
 (** Global universe contexts, names and constraints *)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index e84fce5504..058fa691ee 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,7 +14,6 @@ open Glob_term
 open Constrexpr
 open Vernacexpr
 open Hints
-open ComHints
 
 open Pcoq
 open Pcoq.Prim
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 6ffa88874b..356ccef06b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -142,7 +142,7 @@ let try_declare_scheme what f internal names kn =
     | UndefinedCst s ->
         alarm what internal
           (strbrk "Required constant " ++ str s ++ str " undefined.")
-    | AlreadyDeclared (kind, id) as exn ->
+    | DeclareUniv.AlreadyDeclared (kind, id) as exn ->
       let msg = CErrors.print exn in
       alarm what internal msg
     | DecidabilityMutualNotSupported ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b13e5bf653..838496c595 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -39,17 +39,17 @@ end
 module Info = struct
 
   type t =
-    { hook : DeclareDef.Hook.t option
+    { hook : Declare.Hook.t option
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
-    ; scope : DeclareDef.locality
+    ; scope : Declare.locality
     ; kind : Decls.logical_kind
     (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *)
-    ; thms : DeclareDef.Recthm.t list
+    ; thms : Declare.Recthm.t list
     ; compute_guard : lemma_possible_guards
     }
 
-  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior)
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Declare.Global Declare.ImportDefaultBehavior)
       ?(kind=Decls.(IsProof Lemma)) () =
     { hook
     ; compute_guard = []
@@ -98,7 +98,7 @@ let initialize_named_context_for_proof () =
 
 let add_first_thm ~info ~name ~typ ~impargs =
   let thms =
-    { DeclareDef.Recthm.name
+    { Declare.Recthm.name
     ; impargs
     ; typ = EConstr.Unsafe.to_constr typ
     ; args = [] } :: info.Info.thms
@@ -128,7 +128,7 @@ let start_dependent_lemma ~name ~poly
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun { DeclareDef.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
+    match List.map (fun { Declare.Recthm.name; typ } -> name, (EConstr.of_constr typ)) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
@@ -136,12 +136,12 @@ let rec_tac_initializer finite guard thms snl =
     let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun { DeclareDef.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
+    in match List.map2 (fun { Declare.Recthm.name; typ } n -> (name, n, (EConstr.of_constr typ))) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
 let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
-  let intro_tac { DeclareDef.Recthm.args; _ } = Tactics.auto_intros_tac args in
+  let intro_tac { Declare.Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_terms) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
@@ -161,7 +161,7 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { DeclareDef.Recthm.name; typ; impargs; _} :: thms ->
+  | { Declare.Recthm.name; typ; impargs; _} :: thms ->
     let info =
       Info.{ hook
            ; compute_guard
@@ -200,7 +200,7 @@ module MutualEntry : sig
 
 end = struct
 
-  (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *)
+  (* XXX: Refactor this with the code in [Declare.declare_mutdef] *)
   let guess_decreasing env possible_indexes ((body, ctx), eff) =
     let open Constr in
     match Constr.kind body with
@@ -220,7 +220,7 @@ end = struct
         Pp.(str "Not a proof by induction: " ++
             Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
 
-  let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} =
+  let declare_mutdef ~uctx ~info pe i Declare.Recthm.{ name; impargs; typ; _} =
     let { Info.hook; scope; kind; compute_guard; _ } = info in
     (* if i = 0 , we don't touch the type; this is for compat
        but not clear it is the right thing to do.
@@ -238,7 +238,7 @@ end = struct
         Declare.Internal.map_entry_body pe
           ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
     in
-    DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
+    Declare.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
 
   let declare_mutdef ~info ~uctx const =
     let pe = match info.Info.compute_guard with
@@ -256,8 +256,8 @@ end = struct
   let declare_variable ~info ~uctx pe =
     let { Info.scope; hook } = info in
     List.map_i (
-      fun i { DeclareDef.Recthm.name; typ; impargs } ->
-        DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+      fun i { Declare.Recthm.name; typ; impargs } ->
+        Declare.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
     ) 0 info.Info.thms
 
 end
@@ -395,8 +395,8 @@ let process_idopt_for_save ~idopt info =
     (* Save foo was used; we override the info in the first theorem *)
     let thms =
       match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
-      | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular ->
-        [ { decl with DeclareDef.Recthm.name = save_name } ]
+      | [ { Declare.Recthm.name; _} as decl ], Proof_ending.Regular ->
+        [ { decl with Declare.Recthm.name = save_name } ]
       | _ ->
         err_save_forbidden_in_place_of_qed ()
     in { info with Info.thms }
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index bd2e87ac3a..b1462f1ce5 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -49,11 +49,11 @@ module Info : sig
   type t
 
   val make
-    :  ?hook: DeclareDef.Hook.t
+    :  ?hook: Declare.Hook.t
     (** Callback to be executed at the end of the proof *)
     -> ?proof_ending : Proof_ending.t
     (** Info for special constants *)
-    -> ?scope : DeclareDef.locality
+    -> ?scope : Declare.locality
     (** locality  *)
     -> ?kind:Decls.logical_kind
     (** Theorem, etc... *)
@@ -85,14 +85,14 @@ type lemma_possible_guards = int list list
 
 (** Pretty much internal, used by the Lemma / Fixpoint vernaculars *)
 val start_lemma_with_initialization
-  :  ?hook:DeclareDef.Hook.t
+  :  ?hook:Declare.Hook.t
   -> poly:bool
-  -> scope:DeclareDef.locality
+  -> scope:Declare.locality
   -> kind:Decls.logical_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * Constr.t option list option) option
-  -> DeclareDef.Recthm.t list
+  -> Declare.Recthm.t list
   -> int list option
   -> t
 
diff --git a/vernac/locality.ml b/vernac/locality.ml
index 9e784c8bb3..f62eed5e41 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -34,7 +34,7 @@ let warn_local_declaration =
         strbrk "available without qualification when imported.")
 
 let enforce_locality_exp locality_flag discharge =
-  let open DeclareDef in
+  let open Declare in
   let open Vernacexpr in
   match locality_flag, discharge with
   | Some b, NoDischarge -> Global (importability_of_bool b)
diff --git a/vernac/locality.mli b/vernac/locality.mli
index 26149cb394..bf65579efd 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -20,7 +20,7 @@
 
 val make_locality : bool option -> bool
 val make_non_locality : bool option -> bool
-val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality
+val enforce_locality_exp : bool option -> Vernacexpr.discharge -> Declare.locality
 val enforce_locality : bool option -> bool
 
 (** For commands whose default is to not discharge but to export:
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index bed593234b..5e746afc74 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -162,13 +162,13 @@ let rec solve_obligation prg num tac =
         ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
   in
   let obl = subst_deps_obl obls obl in
-  let scope = DeclareDef.(Global Declare.ImportNeedQualified) in
+  let scope = Declare.(Global Declare.ImportNeedQualified) in
   let kind = kind_of_obligation (snd obl.obl_status) in
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
-  let hook = DeclareDef.Hook.make (DeclareObl.obligation_hook prg obl num auto) in
+  let hook = Declare.Hook.make (DeclareObl.obligation_hook prg obl num auto) in
   let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
   let poly = prg.prg_poly in
   let lemma = Lemmas.start_lemma ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
@@ -309,7 +309,7 @@ let show_term n =
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
 let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
-                   ?(impargs=[]) ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
+                   ?(impargs=[]) ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let info = Id.print name ++ str " has type-checked" in
   let prg = ProgramDecl.make ~opaque name ~udecl term t ~uctx [] None [] obls ~impargs ~poly ~scope ~kind reduce ?hook in
@@ -328,11 +328,11 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
         | _ -> res)
 
 let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
-                           ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
+                           ~poly ?(scope=Declare.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
-  let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in
+  let deps = List.map (fun ({ Declare.Recthm.name; _ }, _, _) -> name) l in
     List.iter
-    (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) ->
+    (fun ({ Declare.Recthm.name; typ; impargs; _ }, b, obls) ->
      let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind)
        notations obls ~impargs ~poly ~scope ~kind reduce ?hook
      in progmap_add name (CEphemeron.create prg)) l;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index f42d199e18..89ed4c3498 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -77,11 +77,11 @@ val add_definition :
   -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?impargs:Impargs.manual_implicits
   -> poly:bool
-  -> ?scope:DeclareDef.locality
+  -> ?scope:Declare.locality
   -> ?kind:Decls.definition_object_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
-  -> ?hook:DeclareDef.Hook.t
+  -> ?hook:Declare.Hook.t
   -> ?opaque:bool
   -> RetrieveObl.obligation_info
   -> DeclareObl.progress
@@ -91,15 +91,15 @@ val add_definition :
 (** Start a [Program Fixpoint] declaration, similar to the above,
    except it takes a list now. *)
 val add_mutual_definitions :
-     (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
+     (Declare.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
   -> uctx:UState.t
   -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
-  -> ?scope:DeclareDef.locality
+  -> ?scope:Declare.locality
   -> ?kind:Decls.definition_object_kind
   -> ?reduce:(constr -> constr)
-  -> ?hook:DeclareDef.Hook.t
+  -> ?hook:Declare.Hook.t
   -> ?opaque:bool
   -> Vernacexpr.decl_notation list
   -> DeclareObl.fixpoint_kind
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f1aae239aa..b97cdfa51c 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -185,7 +185,7 @@ open Pputils
     | [] -> mt()
     | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
-  let pr_reference_or_constr pr_c = let open ComHints in function
+  let pr_reference_or_constr pr_c = function
     | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
@@ -202,7 +202,6 @@ open Pputils
     let opth = pr_opt_hintbases db  in
     let pph =
       let open Hints in
-      let open ComHints in
       match h with
         | HintsResolve l ->
           keyword "Resolve " ++ prlist_with_sep sep
@@ -792,7 +791,6 @@ let string_of_definition_object_kind = let open Decls in function
         return (keyword "Admitted")
 
       | VernacEndProof (Proved (opac,o)) -> return (
-        let open Declare in
         match o with
           | None -> (match opac with
               | Transparent -> keyword "Defined"
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 2b6beaf2e3..1718024edd 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -28,7 +28,7 @@ module Vernac_ :
     val command_entry : vernac_expr Entry.t
     val main_entry : vernac_control option Entry.t
     val red_expr : raw_red_expr Entry.t
-    val hint_info : ComHints.hint_info_expr Entry.t
+    val hint_info : hint_info_expr Entry.t
   end
 
 (* To be removed when the parser is made functional wrt the tactic
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 6d5d16d94a..618a61f487 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,16 +9,15 @@ Himsg
 Locality
 Egramml
 Vernacextend
-Declare
-ComHints
 Ppvernac
 Proof_using
 Egramcoq
 Metasyntax
 DeclareUniv
 RetrieveObl
-DeclareDef
+Declare
 DeclareObl
+ComHints
 Canonical
 RecLemmas
 Library
@@ -48,3 +47,4 @@ Vernacstate
 Vernacinterp
 Proof_global
 Pfedit
+DeclareDef
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index df94f69cf6..aac0b54ed4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -460,7 +460,7 @@ let vernac_custom_entry ~module_local s =
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || Termops.is_section_variable id ||
-     locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> Declare.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
@@ -504,7 +504,7 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms =
   let recguard,thms,snl = RecLemmas.look_for_possibly_mutual_statements evd thms in
   let evd = Evd.minimize_universes evd in
   let thms = List.map (fun (name, (typ, (args, impargs))) ->
-      { DeclareDef.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
+      { Declare.Recthm.name; typ = EConstr.to_constr evd typ; args; impargs} ) thms in
   let () =
     let open UState in
     if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
@@ -521,13 +521,13 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in
 | Coercion ->
   Some (ComCoercion.add_coercion_hook ~poly)
 | CanonicalStructure ->
-  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | SubClass ->
   Some (ComCoercion.add_subclass_hook ~poly)
 | Definition when canonical_instance ->
-  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
+  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure ?local dref)))
 | Let when canonical_instance ->
-  Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
+  Some (Declare.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
 | _ -> None
 
 let default_thm_id = Id.of_string "Unnamed_thm"
@@ -542,7 +542,7 @@ let vernac_definition_name lid local =
          CAst.make ?loc (fresh_name_for_anonymous_theorem ())
     | { v = Name.Name n; loc } -> CAst.make ?loc n in
   let () =
-    let open DeclareDef in
+    let open Declare in
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
     | Global _ -> Dumpglob.dump_definition lid false "def"
@@ -603,8 +603,8 @@ let vernac_assumption ~atts discharge kind l nl =
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
           match scope with
-            | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax"
-            | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+            | Declare.Global _ -> Dumpglob.dump_definition lid false "ax"
+            | Declare.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
 let is_polymorphic_inductive_cumulativity =
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index b65a0da1cc..b622fd9801 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -195,10 +195,12 @@ type syntax_modifier =
   | SetOnlyPrinting
   | SetFormat of string * lstring
 
+type opacity_flag = Opaque | Transparent
+
 type proof_end =
   | Admitted
   (*                         name in `Save ident` when closing goal *)
-  | Proved of Declare.opacity_flag * lident option
+  | Proved of opacity_flag * lident option
 
 type scheme =
   | InductionScheme of bool * qualid or_by_notation * sort_expr
@@ -286,6 +288,22 @@ type extend_name =
 
 type discharge = DoDischarge | NoDischarge
 
+type hint_info_expr = Constrexpr.constr_pattern_expr Typeclasses.hint_info_gen
+
+type reference_or_constr =
+  | HintsReference of Libnames.qualid
+  | HintsConstr of Constrexpr.constr_expr
+
+type hints_expr =
+  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
+  | HintsResolveIFF of bool * Libnames.qualid list * int option
+  | HintsImmediate of reference_or_constr list
+  | HintsUnfold of Libnames.qualid list
+  | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
+  | HintsMode of Libnames.qualid * Hints.hint_mode list
+  | HintsConstructors of Libnames.qualid list
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+
 type nonrec vernac_expr =
 
   | VernacLoad of verbose_flag * string
@@ -336,18 +354,18 @@ type nonrec vernac_expr =
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
       (bool * constr_expr) option * (* body (bool=true when using {}) *)
-      ComHints.hint_info_expr
+      hint_info_expr
 
   | VernacDeclareInstance of
       ident_decl * (* name *)
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
-      ComHints.hint_info_expr
+      hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacExistingInstance of
-    (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *)
+    (qualid * hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacExistingClass of qualid (* inductive or definition name *)
 
@@ -387,7 +405,7 @@ type nonrec vernac_expr =
   (* Commands *)
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * qualid list
-  | VernacHints of string list * ComHints.hints_expr
+  | VernacHints of string list * hints_expr
   | VernacSyntacticDefinition of
       lident * (Id.t list * constr_expr) *
       onlyparsing_flag