Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

9 files changed, 104 insertions, 90 deletions

diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e4fa5e84b4..465f736032 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -86,10 +86,10 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let name_op_to_name ~name_op ~name ~goal_kind suffix =
+let name_op_to_name ~name_op ~name suffix =
   match name_op with
-  | Some s -> s, goal_kind
-  | None -> Nameops.add_suffix name suffix, goal_kind
+  | Some s -> s
+  | None -> Nameops.add_suffix name suffix
 
 let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
@@ -102,10 +102,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      redundancy on constant declaration. This opens up an interesting
      question, how does abstract behave when discharge is local for example?
   *)
-  let goal_kind, suffix = if opaque
-    then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
-    else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
-  let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
+  let suffix = if opaque
+    then "_subproof"
+    else "_subterm" in
+  let name = name_op_to_name ~name_op ~name suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -121,7 +121,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
         then (s1,push_named_context_val d s2)
         else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, Environ.empty_named_context_val) in
-  let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in
+  let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in
   let concl = match goal_type with
               | None ->  Proofview.Goal.concl gl
               | Some ty -> ty in
@@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
+    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 339d4de2a0..499e7a63d7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv poly (c, _, ctx) clenv gl =
+let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
      below just replaces the metas of sigma by those coming from the clenv. *)
@@ -95,22 +95,22 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
+let unify_resolve ~poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv poly c clenv gl in
+  let clenv, c = connect_hint_clenv ~poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
 
-let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
+let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
 
-let unify_resolve_gen poly = function
+let unify_resolve_gen ~poly = function
   | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve poly flags
+  | Some flags -> unify_resolve ~poly flags
 
 let exact poly (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -378,12 +378,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
+    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
     | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen poly flags (c,cl))
+        (unify_resolve_gen ~poly flags (c,cl))
 	(* With "(debug) trivial", we shouldn't end here, and
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a834b4b12d..5ae63be539 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -14,7 +14,6 @@ open Names
 open EConstr
 open Clenv
 open Pattern
-open Decl_kinds
 open Hints
 open Tactypes
 
@@ -24,11 +23,11 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
-val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  Proofview.Goal.t -> clausenv * constr
+val connect_hint_clenv
+  : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
+val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b0fb47726a..303ddacb67 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -204,11 +204,11 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   end
 
 let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv', c = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
 let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv', _ = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
@@ -536,7 +536,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
               make_resolves env sigma ~name:(PathHints path)
-                  (true,false,not !Flags.quiet) info false
+                  (true,false,not !Flags.quiet) info ~poly:false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
@@ -544,8 +544,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
         (hints @ List.map_filter
          (fun f -> try Some (f (c, cty, Univ.ContextSet.empty))
            with Failure _ | UserError _ -> None)
-         [make_exact_entry ~name env sigma pri false;
-          make_apply_entry ~name env sigma flags pri false])
+         [make_exact_entry ~name env sigma pri ~poly:false;
+          make_apply_entry ~name env sigma flags pri ~poly:false])
     else []
 
 let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/declare.ml b/tactics/declare.ml
index ca5d265733..4a4e2cf60a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -33,6 +33,8 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -96,7 +98,7 @@ let cache_constant ((sp,kn), obj) =
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
+  add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
@@ -262,23 +264,23 @@ let declare_definition ?(internal=UserIndividualRequest)
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(p,d,mk)) ->
+  | Inr (id,(path,d,kind)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
     alreadydeclared (Id.print id ++ str " already exists");
 
-  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty,poly),ctx) in
+  let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;univs;poly;impl} ->
+      let () = Global.push_named_assum ((id,typ,poly),univs) in
       let impl = if impl then Implicit else Explicit in
-        impl, true, poly, ctx
+        impl, true, poly, univs
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -305,8 +307,8 @@ let cache_variable ((sp,_),o) =
       Explicit, de.proof_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
-  add_variable_data id (p,opaq,ctx,poly,mk)
+  add_section_variable ~name:id ~kind:impl ~poly univs;
+  add_variable_data id {path;opaque;univs;poly;kind}
 
 let discharge_variable (_,o) = match o with
   | Inr (id,_) ->
@@ -374,7 +376,7 @@ let cache_inductive ((sp,kn),mie) =
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
+  add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),mie) =
@@ -525,7 +527,7 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
     ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
     ~discharge:(fun (_, x) -> Some x)
 
-let declare_universe_context poly ctx =
+let declare_universe_context ~poly ctx =
   if poly then
     (Global.push_context_set true ctx; Lib.add_section_context ctx)
   else
@@ -605,7 +607,7 @@ let declare_univ_binders gr pl =
     in
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
-let do_universe poly l =
+let do_universe ~poly l =
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
@@ -616,11 +618,11 @@ let do_universe poly l =
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-  let () = declare_universe_context poly ctx in
+  let () = declare_universe_context ~poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   Lib.add_anonymous_leaf (input_univ_names (src, l))
 
-let do_constraint poly l =
+let do_constraint ~poly l =
   let open Univ in
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
@@ -647,4 +649,4 @@ let do_constraint poly l =
     Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  declare_universe_context poly uctx
+  declare_universe_context ~poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0a2332748c..d87c096119 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -24,7 +24,7 @@ open Decl_kinds
 
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a Proof_global.proof_entry
@@ -51,6 +51,8 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?univs:Entries.universes_entry ->
   ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration
@@ -92,7 +94,7 @@ val exists_name : Id.t -> bool
 (** Global universe contexts, names and constraints *)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
-val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 
-val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
+val do_universe : poly:bool -> lident list -> unit
+val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ac6253cf40..cc3e78f3b8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -113,7 +113,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv poly c clenv gl in
+      let clenv', c = connect_hint_clenv ~poly c clenv gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -131,7 +131,7 @@ let hintmap_of sigma secvars hdc concl =
 
 let e_exact poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -168,7 +168,7 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl =
       in
       (b,
         let tac = function
-        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
         | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
         | Give_exact (c,cl) -> e_exact poly st (c,cl)
         | Res_pf_THEN_trivial_fail (term,cl) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e824c4bd64..014e54158d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -27,7 +27,6 @@ open Smartlocate
 open Termops
 open Inductiveops
 open Typing
-open Decl_kinds
 open Typeclasses
 open Pattern
 open Patternops
@@ -142,15 +141,22 @@ type raw_hint = constr * types * Univ.ContextSet.t
 
 type hint = (raw_hint * clausenv) hint_ast with_uid
 
-type 'a with_metadata = {
-  pri     : int;            (* A number lower is higher priority *)
-  poly    : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat     : constr_pattern option; (* A pattern for the concl of the Goal *)
-  name    : hints_path_atom; (* A potential name to refer to the hint *)
-  db : string option; (** The database from which the hint comes *)
-  secvars : Id.Pred.t; (* The set of section variables the hint depends on *)
-  code    : 'a;     (* the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata =
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -792,7 +798,7 @@ let secvars_of_constr env sigma c =
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global env gr)
 
-let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
     match EConstr.kind sigma cty with
@@ -813,7 +819,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
 	   db = None; secvars;
 	   code = with_uid (Give_exact (c, cty, ctx)); })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
   match EConstr.kind sigma cty with
   | Prod _ ->
@@ -887,18 +893,18 @@ 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 false ctx;
+      Declare.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags info poly ?name cr =
+let make_resolves env sigma flags info ~poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-			     [make_exact_entry env sigma info poly ?name;
-			      make_apply_entry env sigma flags info poly ?name]
+                             [make_exact_entry env sigma info ~poly ?name;
+                              make_apply_entry env sigma flags info ~poly ?name]
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
@@ -912,7 +918,7 @@ let make_resolve_hyp env sigma decl =
   let hname = NamedDecl.get_id decl in
   let c = mkVar hname in
   try
-    [make_apply_entry env sigma (true, true, false) empty_hint_info false
+    [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false
        ~name:(PathHints [VarRef hname])
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
@@ -1178,7 +1184,7 @@ let add_resolves env sigma clist local dbnames =
       let r =
         List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
           make_resolves env sigma (true,hnf,not !Flags.quiet)
-            pri poly ~name:path gr) clist)
+            pri ~poly ~name:path gr) clist)
       in
       let hint = make_hint ~local dbname (AddHints r) in
       Lib.add_anonymous_leaf (inAutoHint hint))
@@ -1238,8 +1244,8 @@ type hnf = bool
 type nonrec hint_info = hint_info
 
 type hints_entry =
-  | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -1286,7 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Declare.declare_universe_context false diff;
+    else (Declare.declare_universe_context ~poly:false diff;
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let project_hint ~poly pri l2r r =
@@ -1318,7 +1324,7 @@ let project_hint ~poly pri l2r r =
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
 
-let interp_hints poly =
+let interp_hints ~poly =
   fun h ->
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -1417,7 +1423,7 @@ let expand_constructor_hints env sigma lems =
 let constructor_hints env sigma eapply lems =
   let lems = expand_constructor_hints env sigma lems in
   List.map_append (fun (poly, lem) ->
-      make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
+      make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems
 
 let make_local_hint_db env sigma ts eapply lems =
   let map c = c env sigma in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 839ef31189..4c82a068b1 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
 open Names
 open EConstr
 open Environ
-open Decl_kinds
 open Evd
 open Tactypes
 open Clenv
@@ -54,15 +53,22 @@ type 'a hints_path_atom_gen =
 type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
-type 'a with_metadata = private {
-  pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
-  poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
-  name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  db    : hint_db_name option;
-  secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *)
-  code    : 'a; (** the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata = private
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -176,9 +182,8 @@ type hint_term =
   | IsConstr of constr * Univ.ContextSet.t
 
 type hints_entry =
-  | HintsResolveEntry of
-    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -202,7 +207,7 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : polymorphic -> hints_expr -> hints_entry
+val interp_hints : poly:bool -> hints_expr -> hints_entry
 
 val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
@@ -219,7 +224,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
    [hint_pattern] is the hint's desired pattern, it is inferred if not specified
 *)
 
-val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
@@ -237,7 +242,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint
 *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -248,7 +253,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].