Merge PR #12130: [declare] [tactics] Move declare to `vernac`

Reviewed-by: ppedrot

31 files changed, 327 insertions, 238 deletions

diff --git a/dev/base_include b/dev/base_include
index 96a867475d..45e79147c1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -129,7 +129,7 @@ open Elim
 open Equality
 open Hipattern
 open Inv
-open Leminv
+open Ltac_plugin.Leminv
 open Tacticals
 open Tactics
 open Eqschemes
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7754fe401e..0bad3cbe5b 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
         else (* This is a global universe context that shouldn't be
                 refreshed at every use of the hint, declare it globally. *)
-          (Declare.declare_universe_context ~poly:false ctx;
+          (DeclareUctx.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index e713ab13b2..5baa23b3e9 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 ->
-        { Hints.HintsExtern (n,c, in_tac tac) } ] ]
+        { ComHints.HintsExtern (n,c, in_tac tac) } ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
diff --git a/tactics/leminv.ml b/plugins/ltac/leminv.ml
index 5a8ec404ee..5a8ec404ee 100644
--- a/tactics/leminv.ml
+++ b/plugins/ltac/leminv.ml
diff --git a/tactics/leminv.mli b/plugins/ltac/leminv.mli
index 5a5de7b58f..5a5de7b58f 100644
--- a/tactics/leminv.mli
+++ b/plugins/ltac/leminv.mli
diff --git a/plugins/ltac/ltac_plugin.mlpack b/plugins/ltac/ltac_plugin.mlpack
index e83eab20dc..f31361279c 100644
--- a/plugins/ltac/ltac_plugin.mlpack
+++ b/plugins/ltac/ltac_plugin.mlpack
@@ -9,6 +9,7 @@ Tactic_debug
 Tacintern
 Profile_ltac
 Tactic_matching
+Leminv
 Tacinterp
 Tacentries
 Evar_tactics
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0646af3552..633cdbd735 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,7 +150,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
-  let () = Declare.declare_universe_context ~poly:false univs in
+  let () = DeclareUctx.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant ~name:(Id.of_string na)
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index 0e78a03f45..6b575d0807 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -40,6 +40,9 @@ let name_op_to_name ~name_op ~name suffix =
   | Some s -> s
   | None -> Nameops.add_suffix name suffix
 
+let declare_abstract = ref (fun ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl ->
+  CErrors.anomaly (Pp.str "Abstract declaration hook not registered"))
+
 let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
   let open Tacmach.New in
@@ -77,7 +80,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let concl = it_mkNamedProd_or_LetIn concl sign in
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let effs, sigma, lem, args, safe =
-    Declare.declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
+    !declare_abstract ~name ~poly ~sign ~secsign ~kind ~opaque ~solve_tac sigma concl in
   let solve =
     Proofview.tclEFFECTS effs <*>
     tacK lem args
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 5c936ff9d6..a138a457b3 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,15 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+val declare_abstract :
+  (  name:Names.Id.t
+  -> poly:bool
+  -> kind:Decls.logical_kind
+  -> sign:EConstr.named_context
+  -> secsign:Environ.named_context_val
+  -> opaque:bool
+  -> solve_tac:unit Proofview.tactic
+  -> Evd.evar_map
+  -> EConstr.t
+  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool) ref
diff --git a/tactics/declareUctx.ml b/tactics/declareUctx.ml
new file mode 100644
index 0000000000..3f67ff20a4
--- /dev/null
+++ b/tactics/declareUctx.ml
@@ -0,0 +1,34 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+(** Monomorphic universes need to survive sections. *)
+
+let name_instance inst =
+  let map lvl = match Univ.Level.name lvl with
+    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
+      assert false
+    | Some na ->
+      try
+        let qid = Nametab.shortest_qualid_of_universe na in
+        Names.Name (Libnames.qualid_basename qid)
+      with Not_found ->
+        (* Best-effort naming from the string representation of the level.
+           See univNames.ml for a similar hack. *)
+        Names.Name (Names.Id.of_string_soft (Univ.Level.to_string lvl))
+  in
+  Array.map map (Univ.Instance.to_array inst)
+
+let declare_universe_context ~poly ctx =
+  if poly then
+    let uctx = Univ.ContextSet.to_context ctx in
+    let nas = name_instance (Univ.UContext.instance uctx) in
+    Global.push_section_context (nas, uctx)
+  else
+    Global.push_context_set ~strict:true ctx
diff --git a/tactics/declareUctx.mli b/tactics/declareUctx.mli
new file mode 100644
index 0000000000..7ecfab04f2
--- /dev/null
+++ b/tactics/declareUctx.mli
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   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)         *)
+(************************************************************************)
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
diff --git a/tactics/hints.ml b/tactics/hints.ml
index ffb0e030db..5fb519cc4f 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -23,7 +23,6 @@ open Globnames
 open Libobject
 open Namegen
 open Libnames
-open Smartlocate
 open Termops
 open Inductiveops
 open Typeclasses
@@ -100,8 +99,6 @@ let empty_hint_info =
 (*           The Type of Constructions Autotactic Hints                 *)
 (************************************************************************)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -164,10 +161,6 @@ type full_hint = hint with_metadata
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
 
-type reference_or_constr =
-  | HintsReference of qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -178,16 +171,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-type hints_expr =
-  | HintsResolve of (hint_info_expr * bool * reference_or_constr) list
-  | HintsResolveIFF of bool * qualid list * int option
-  | HintsImmediate of reference_or_constr list
-  | HintsUnfold of qualid list
-  | HintsTransparency of qualid hints_transparency_target * bool
-  | HintsMode of qualid * hint_mode list
-  | HintsConstructors of qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type import_level = HintLax | HintWarn | HintStrict
 
 let warn_hint_to_string = function
@@ -895,7 +878,7 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Declare.declare_universe_context ~poly:false ctx;
+      DeclareUctx.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
@@ -1310,114 +1293,6 @@ let prepare_hint check env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     (c', diff)
 
-let project_hint ~poly pri l2r r =
-  let open EConstr in
-  let open Coqlib in
-  let gr = Smartlocate.global_with_alias r in
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, c = Evd.fresh_global env sigma gr in
-  let t = Retyping.get_type_of env sigma c in
-  let t =
-    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in
-  let sign,ccl = decompose_prod_assum sigma t in
-  let (a,b) = match snd (decompose_app sigma ccl) with
-    | [a;b] -> (a,b)
-    | _ -> assert false in
-  let p =
-    if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
-  let sigma, p = Evd.fresh_global env sigma p in
-  let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in
-  let c = it_mkLambda_or_LetIn
-    (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in
-  let name =
-    Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
-  in
-  let ctx = Evd.univ_entry ~poly sigma in
-  let c = EConstr.to_constr sigma c in
-  let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in
-  let c = Declare.declare_constant
-      ~local:Declare.ImportDefaultBehavior
-      ~name ~kind:Decls.(IsDefinition Definition) cb
-  in
-  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
-    (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c))
-
-let warn_deprecated_hint_constr =
-  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
-         (fun () ->
-           Pp.strbrk
-             "Declaring arbitrary terms as hints is deprecated; declare a global reference instead"
-         )
-
-let interp_hints ~poly =
-  fun h ->
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
-  let f poly c =
-    let evd,c = Constrintern.interp_open_constr env sigma c in
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    let (c, diff) = prepare_hint true env sigma (evd,c) in
-    if poly then IsConstr (c, diff)
-    else
-      let () = Declare.declare_universe_context ~poly:false diff in
-      IsConstr (c, Univ.ContextSet.empty)
-  in
-  let fref r =
-    let gr = global_with_alias r in
-    Dumpglob.add_glob ?loc:r.CAst.loc gr;
-    gr in
-  let fr r = evaluable_of_global_reference env (fref r) in
-  let fi c =
-    match c with
-    | HintsReference c ->
-      let gr = global_with_alias c in
-        (PathHints [gr], poly, IsGlobRef gr)
-    | HintsConstr c ->
-      let () = warn_deprecated_hint_constr () in
-      (PathAny, poly, f poly c)
-  in
-  let fp = Constrintern.intern_constr_pattern env sigma in
-  let fres (info, b, r) =
-    let path, poly, gr = fi r in
-    let info = { info with hint_pattern = Option.map fp info.hint_pattern } in
-      (info, poly, b, path, gr)
-  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
-  match h with
-  | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
-  | HintsResolveIFF (l2r, lc, n) ->
-    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
-  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
-  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
-  | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
-  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
-  | HintsConstructors lqid ->
-      let constr_hints_of_ind qid =
-        let ind = global_inductive_with_alias qid in
-        let mib,_ = Global.lookup_inductive ind in
-        Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
-          List.init (nconstructors env ind)
-            (fun i -> let c = (ind,i+1) in
-                      let gr = GlobRef.ConstructRef c in
-                        empty_hint_info,
-                        (Declareops.inductive_is_polymorphic mib), true,
-                        PathHints [gr], IsGlobRef gr)
-      in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
-  | HintsExtern (pri, patcom, tacexp) ->
-      let pat =	Option.map (fp sigma) patcom in
-      let l = match pat with None -> [] | Some (l, _) -> l in
-      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
-      let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in
-      let _, tacexp = Genintern.generic_intern env tacexp in
-      HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
-
 let add_hints ~locality dbnames h =
   let local, superglobal = match locality with
   | Goptions.OptDefault | Goptions.OptGlobal -> false, true
@@ -1562,8 +1437,7 @@ let pr_hint_term env sigma cl =
 (* print all hints that apply to the concl of the current goal *)
 let pr_applicable_hint pf =
   let env = Global.env () in
-  let pts = Declare.Proof.get_proof pf in
-  let Proof.{goals;sigma} = Proof.data pts in
+  let Proof.{goals;sigma} = Proof.data pf in
   match goals with
   | [] -> CErrors.user_err Pp.(str "No focused goal.")
   | g::_ ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index eed0e37fac..f5fd3348e4 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -32,8 +32,6 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen
 
 (** Pre-created hint databases *)
 
-type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen
-
 type 'a hint_ast =
   | Res_pf     of 'a (* Hint Apply *)
   | ERes_pf    of 'a (* Hint EApply *)
@@ -78,10 +76,6 @@ type search_entry
 
 type hint_entry
 
-type reference_or_constr =
-  | HintsReference of Libnames.qualid
-  | HintsConstr of Constrexpr.constr_expr
-
 type hint_mode =
   | ModeInput (* No evars *)
   | ModeNoHeadEvar (* No evar at the head *)
@@ -92,16 +86,6 @@ type 'a hints_transparency_target =
   | HintsConstants
   | HintsReferences of 'a list
 
-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_transparency_target * bool
-  | HintsMode of Libnames.qualid * hint_mode list
-  | HintsConstructors of Libnames.qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
-
 type 'a hints_path_gen =
   | PathAtom of 'a hints_path_atom_gen
   | PathStar of 'a hints_path_gen
@@ -217,8 +201,6 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : poly:bool -> hints_expr -> hints_entry
-
 val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
@@ -306,7 +288,7 @@ val wrap_hint_warning_fun : env -> evar_map ->
 (** Printing  hints *)
 
 val pr_searchtable : env -> evar_map -> Pp.t
-val pr_applicable_hint : Declare.Proof.t -> Pp.t
+val pr_applicable_hint : Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 8336fae02f..e422366ed6 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -86,15 +86,15 @@ let compute_name internal id =
     Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name
   else id
 
+let declare_definition_scheme = ref (fun ~internal ~univs ~role ~name c ->
+    CErrors.anomaly (Pp.str "scheme declaration not registered"))
+
 let define internal role id c poly univs =
   let id = compute_name internal id in
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = Declare.pure_definition_entry ~univs c in
-  let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id entry in
-  let () = if internal then () else Declare.definition_message id in
-  kn, eff
+  !declare_definition_scheme ~internal ~univs ~role ~name:id c
 
 let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) =
   let (c, ctx), eff = f mode ind in
diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli
index dad2036c64..736de2af37 100644
--- a/tactics/ind_tables.mli
+++ b/tactics/ind_tables.mli
@@ -59,3 +59,11 @@ val check_scheme : 'a scheme_kind -> inductive -> bool
 val lookup_scheme : 'a scheme_kind -> inductive -> Constant.t
 
 val pr_scheme_kind : 'a scheme_kind -> Pp.t
+
+val declare_definition_scheme :
+  (internal : bool
+   -> univs:Entries.universes_entry
+   -> role:Evd.side_effect_role
+   -> name:Id.t
+   -> Constr.t
+   -> Constant.t * Evd.side_effects) ref
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 537d111f23..36d61feed1 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -1,5 +1,4 @@
 DeclareScheme
-Declare
 Dnet
 Dn
 Btermdn
@@ -18,7 +17,7 @@ Elim
 Equality
 Contradiction
 Inv
-Leminv
+DeclareUctx
 Hints
 Auto
 Eauto
diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable
new file mode 100644
index 0000000000..ffaa7e70f4
--- /dev/null
+++ b/vernac/.ocamlformat-enable
@@ -0,0 +1 @@
+comHints.ml
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 9698c14452..f410cddfef 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 -> Hints.hint_info_expr option -> unit
+val existing_instance : bool -> qualid -> ComHints.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)
-  -> Hints.hint_info_expr
+  -> ComHints.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)
-  -> Hints.hint_info_expr
+  -> ComHints.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)
-  -> Hints.hint_info_expr
+  -> ComHints.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
-  -> Hints.hint_info_expr
+  -> ComHints.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 43e86fa9bd..776ffd6b9f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -91,7 +91,7 @@ let declare_assumptions ~poly ~scope ~kind univs nl l =
   let () = match scope with
     | Discharge ->
       (* declare universes separately for variables *)
-      Declare.declare_universe_context ~poly (context_set_of_entry (fst univs))
+      DeclareUctx.declare_universe_context ~poly (context_set_of_entry (fst univs))
     | Global _ -> ()
   in
   let _, _ = List.fold_left (fun (subst,univs) ((is_coe,idl),typ,imps) ->
@@ -191,7 +191,7 @@ let context_subst subst (name,b,t,impl) =
 
 let context_insection sigma ~poly ctx =
   let uctx = Evd.universe_context_set sigma in
-  let () = Declare.declare_universe_context ~poly uctx in
+  let () = DeclareUctx.declare_universe_context ~poly uctx in
   let fn subst (name,_,_,_ as d) =
     let d = context_subst subst d in
     let () = match d with
@@ -226,7 +226,7 @@ let context_nosection sigma ~poly ctx =
       (* Multiple monomorphic axioms: declare universes separately to
          avoid redeclaring them. *)
       let uctx = Evd.universe_context_set sigma in
-      let () = Declare.declare_universe_context ~poly uctx in
+      let () = DeclareUctx.declare_universe_context ~poly uctx in
       Monomorphic_entry Univ.ContextSet.empty
   in
   let fn subst d =
diff --git a/vernac/comHints.ml b/vernac/comHints.ml
new file mode 100644
index 0000000000..5a48e9c16c
--- /dev/null
+++ b/vernac/comHints.ml
@@ -0,0 +1,174 @@
+(************************************************************************)
+(*         *   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 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
+  let gr = Smartlocate.global_with_alias r in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let sigma, c = Evd.fresh_global env sigma gr in
+  let t = Retyping.get_type_of env sigma c in
+  let t =
+    Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t
+  in
+  let sign, ccl = decompose_prod_assum sigma t in
+  let a, b =
+    match snd (decompose_app sigma ccl) with
+    | [a; b] -> (a, b)
+    | _ -> assert false
+  in
+  let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in
+  let sigma, p = Evd.fresh_global env sigma p in
+  let c =
+    Reductionops.whd_beta sigma
+      (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign))
+  in
+  let c =
+    it_mkLambda_or_LetIn
+      (mkApp
+         ( p
+         , [| mkArrow a Sorts.Relevant (Vars.lift 1 b)
+            ; mkArrow b Sorts.Relevant (Vars.lift 1 a)
+            ; c |] ))
+      sign
+  in
+  let name =
+    Nameops.add_suffix
+      (Nametab.basename_of_global gr)
+      ("_proj_" ^ if l2r then "l2r" else "r2l")
+  in
+  let ctx = Evd.univ_entry ~poly sigma in
+  let c = EConstr.to_constr sigma c in
+  let cb =
+    Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c))
+  in
+  let c =
+    Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name
+      ~kind:Decls.(IsDefinition Definition)
+      cb
+  in
+  let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
+  (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c))
+
+let warn_deprecated_hint_constr =
+  CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated"
+    (fun () ->
+      Pp.strbrk
+        "Declaring arbitrary terms as hints is deprecated; declare a global \
+         reference instead")
+
+let interp_hints ~poly h =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let f poly c =
+    let evd, c = Constrintern.interp_open_constr env sigma c in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let c, diff = Hints.prepare_hint true env sigma (evd, c) in
+    if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"])
+    else
+      let () = DeclareUctx.declare_universe_context ~poly:false diff in
+      (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"])
+  in
+  let fref r =
+    let gr = Smartlocate.global_with_alias r in
+    Dumpglob.add_glob ?loc:r.CAst.loc gr;
+    gr
+  in
+  let fr r = Tacred.evaluable_of_global_reference env (fref r) in
+  let fi c =
+    let open Hints in
+    match c with
+    | HintsReference c ->
+      let gr = Smartlocate.global_with_alias c in
+      (PathHints [gr], poly, IsGlobRef gr)
+    | HintsConstr c ->
+      let () = warn_deprecated_hint_constr () in
+      (PathAny, poly, f poly c)
+  in
+  let fp = Constrintern.intern_constr_pattern env sigma in
+  let fres (info, b, r) =
+    let path, poly, gr = fi r in
+    let info =
+      { info with
+        Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern
+      }
+    in
+    (info, poly, b, path, gr)
+  in
+  let ft =
+    let open Hints in
+    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) ->
+    HintsResolveEntry (List.map (project_hint ~poly n l2r) lc)
+  | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints)
+  | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints)
+  | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b)
+  | HintsMode (r, l) -> HintsModeEntry (fref r, l)
+  | HintsConstructors lqid ->
+    let constr_hints_of_ind qid =
+      let ind = Smartlocate.global_inductive_with_alias qid in
+      let mib, _ = Global.lookup_inductive ind in
+      Dumpglob.dump_reference ?loc:qid.CAst.loc "<>"
+        (Libnames.string_of_qualid qid)
+        "ind";
+      List.init (Inductiveops.nconstructors env ind) (fun i ->
+          let c = (ind, i + 1) in
+          let gr = Names.GlobRef.ConstructRef c in
+          ( empty_hint_info
+          , Declareops.inductive_is_polymorphic mib
+          , true
+          , PathHints [gr]
+          , IsGlobRef gr ))
+    in
+    HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
+  | HintsExtern (pri, patcom, tacexp) ->
+    let pat = Option.map (fp sigma) patcom in
+    let l = match pat with None -> [] | Some (l, _) -> l in
+    let ltacvars =
+      List.fold_left
+        (fun accu x -> Names.Id.Set.add x accu)
+        Names.Id.Set.empty l
+    in
+    let env = Genintern.{(empty_glob_sign env) with ltacvars} in
+    let _, tacexp = Genintern.generic_intern env tacexp in
+    HintsExternEntry
+      ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp)
diff --git a/vernac/comHints.mli b/vernac/comHints.mli
new file mode 100644
index 0000000000..77fbef5387
--- /dev/null
+++ b/vernac/comHints.mli
@@ -0,0 +1,29 @@
+(************************************************************************)
+(*         *   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 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
diff --git a/tactics/declare.ml b/vernac/declare.ml
index cce43e833e..366dd2d026 100644
--- a/tactics/declare.ml
+++ b/vernac/declare.ml
@@ -133,31 +133,6 @@ let _ = CErrors.register_handler (function
 
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
-(** Monomorphic universes need to survive sections. *)
-
-let name_instance inst =
-  let map lvl = match Univ.Level.name lvl with
-    | None -> (* Having Prop/Set/Var as section universes makes no sense *)
-      assert false
-    | Some na ->
-      try
-        let qid = Nametab.shortest_qualid_of_universe na in
-        Name (Libnames.qualid_basename qid)
-      with Not_found ->
-        (* Best-effort naming from the string representation of the level.
-           See univNames.ml for a similar hack. *)
-        Name (Id.of_string_soft (Univ.Level.to_string lvl))
-  in
-  Array.map map (Univ.Instance.to_array inst)
-
-let declare_universe_context ~poly ctx =
-  if poly then
-    let uctx = Univ.ContextSet.to_context ctx in
-    let nas = name_instance (Univ.UContext.instance uctx) in
-    Global.push_section_context (nas, uctx)
-  else
-    Global.push_context_set ~strict:true ctx
-
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -589,7 +564,7 @@ let declare_variable ~name ~kind d =
       let univs = Univ.ContextSet.union body_ui entry_ui in
       (* We must declare the universe constraints before type-checking the
          term. *)
-      let () = declare_universe_context ~poly univs in
+      let () = DeclareUctx.declare_universe_context ~poly univs in
       let se = {
         Entries.secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
@@ -899,3 +874,15 @@ module Proof = struct
   let update_global_env = update_global_env
   let get_open_goals = get_open_goals
 end
+
+let declare_definition_scheme ~internal ~univs ~role ~name c =
+  let kind = Decls.(IsDefinition Scheme) in
+  let entry = pure_definition_entry ~univs c in
+  let kn, eff = declare_private_constant ~role ~kind ~name entry in
+  let () = if internal then () else definition_message name in
+  kn, eff
+
+let _ = Ind_tables.declare_definition_scheme := declare_definition_scheme
+let _ = Abstract.declare_abstract := declare_abstract
+
+let declare_universe_context = DeclareUctx.declare_universe_context
diff --git a/tactics/declare.mli b/vernac/declare.mli
index 1fabf80b2a..e23e148ddc 100644
--- a/tactics/declare.mli
+++ b/vernac/declare.mli
@@ -135,8 +135,6 @@ type 'a constant_entry =
   | ParameterEntry of parameter_entry
   | PrimitiveEntry of primitive_entry
 
-val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
-
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
@@ -162,16 +160,6 @@ val definition_entry
   -> constr
   -> Evd.side_effects proof_entry
 
-(** XXX: Scheduled for removal from public API, use `DeclareDef` instead *)
-val pure_definition_entry
-  : ?fix_exn:Future.fix_exn
-  -> ?opaque:bool
-  -> ?inline:bool
-  -> ?types:types
-  -> ?univs:Entries.universes_entry
-  -> constr
-  -> unit proof_entry
-
 type import_status = ImportDefaultBehavior | ImportNeedQualified
 
 (** [declare_constant id cd] declares a global declaration
@@ -189,14 +177,6 @@ val declare_constant
   -> Evd.side_effects constant_entry
   -> Constant.t
 
-val declare_private_constant
-  :  ?role:Evd.side_effect_role
-  -> ?local:import_status
-  -> name:Id.t
-  -> kind:Decls.logical_kind
-  -> unit proof_entry
-  -> Constant.t * Evd.side_effects
-
 (** [inline_private_constants ~sideff ~uctx env ce] will inline the
    constants in [ce]'s body and return the body plus the updated
    [UState.t].
@@ -262,19 +242,6 @@ val close_future_proof : feedback_id:Stateid.t -> Proof.t -> closed_proof_output
     Returns [false] if an unsafe tactic has been used. *)
 val by : unit Proofview.tactic -> Proof.t -> Proof.t * bool
 
-(** Declare abstract constant; will check no evars are possible; *)
-val declare_abstract :
-     name:Names.Id.t
-  -> poly:bool
-  -> kind:Decls.logical_kind
-  -> sign:EConstr.named_context
-  -> secsign:Environ.named_context_val
-  -> opaque:bool
-  -> solve_tac:unit Proofview.tactic
-  -> Evd.evar_map
-  -> EConstr.t
-  -> Evd.side_effects * Evd.evar_map * EConstr.t * EConstr.t list * bool
-
 val build_by_tactic
   :  ?side_eff:bool
   -> Environ.env
@@ -312,3 +279,6 @@ val build_constant_by_tactic :
   EConstr.types ->
   unit Proofview.tactic ->
   Evd.side_effects proof_entry * bool * UState.t
+
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
+[@@ocaml.deprecated "Use DeclareUctx.declare_universe_context"]
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml
index 20fa43c8e7..89f3503f4d 100644
--- a/vernac/declareUniv.ml
+++ b/vernac/declareUniv.ml
@@ -94,7 +94,7 @@ let do_universe ~poly l =
   in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in
-  Declare.declare_universe_context ~poly ctx
+  DeclareUctx.declare_universe_context ~poly ctx
 
 let do_constraint ~poly l =
   let open Univ in
@@ -107,4 +107,4 @@ let do_constraint ~poly l =
       Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  Declare.declare_universe_context ~poly uctx
+  DeclareUctx.declare_universe_context ~poly uctx
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 058fa691ee..e84fce5504 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,6 +14,7 @@ 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 7260b13ff6..6ffa88874b 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -91,12 +91,11 @@ let () =
       optwrite = (fun b -> rewriting_flag := b) }
 
 (* Util *)
-
 let define ~poly name sigma c types =
-  let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
   let univs = Evd.univ_entry ~poly sigma in
   let entry = Declare.definition_entry ~univs ?types c in
-  let kn = f ~name (DefinitionEntry entry) in
+  let kind = Decls.(IsDefinition Scheme) in
+  let kn = declare_constant ~kind ~name (DefinitionEntry entry) in
   definition_message name;
   kn
 
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 36d79bfdb1..f1aae239aa 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 Hints in function
+  let pr_reference_or_constr pr_c = let open ComHints in function
     | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
@@ -202,6 +202,7 @@ 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
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4de12f5e3b..2b6beaf2e3 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 : Hints.hint_info_expr Entry.t
+    val hint_info : ComHints.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 b7728fe699..6d5d16d94a 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -9,6 +9,8 @@ Himsg
 Locality
 Egramml
 Vernacextend
+Declare
+ComHints
 Ppvernac
 Proof_using
 Egramcoq
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d84bac5608..df39c617d3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1275,7 +1275,7 @@ let vernac_hints ~atts dbnames h =
       "This command does not support the export attribute in sections.");
   | OptDefault | OptLocal -> ()
   in
-  Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h)
+  Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x only_parsing =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
@@ -1727,7 +1727,8 @@ let vernac_print ~pstate ~atts =
   | PrintHintGoal ->
      begin match pstate with
      | Some pstate ->
-       Hints.pr_applicable_hint pstate
+       let pf = Declare.Proof.get_proof pstate in
+       Hints.pr_applicable_hint pf
      | None ->
        str "No proof in progress"
      end
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index e46186288e..b65a0da1cc 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -336,18 +336,18 @@ type nonrec vernac_expr =
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
       (bool * constr_expr) option * (* body (bool=true when using {}) *)
-      Hints.hint_info_expr
+      ComHints.hint_info_expr
 
   | VernacDeclareInstance of
       ident_decl * (* name *)
       local_binder_expr list * (* binders *)
       constr_expr * (* type *)
-      Hints.hint_info_expr
+      ComHints.hint_info_expr
 
   | VernacContext of local_binder_expr list
 
   | VernacExistingInstance of
-    (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *)
+    (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *)
 
   | VernacExistingClass of qualid (* inductive or definition name *)
 
@@ -387,7 +387,7 @@ type nonrec vernac_expr =
   (* Commands *)
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * qualid list
-  | VernacHints of string list * Hints.hints_expr
+  | VernacHints of string list * ComHints.hints_expr
   | VernacSyntacticDefinition of
       lident * (Id.t list * constr_expr) *
       onlyparsing_flag