Do not export the internals of the prepare_hint function.

This statically ensures more invariants and moves a global declaration out
of this function.

3 files changed, 14 insertions, 18 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2ce32b309a..ef2402489e 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -86,16 +86,13 @@ let rec prolog l n gl =
   let prol = (prolog l (n-1)) in
   (tclFIRST (List.map (fun t -> (tclTHEN t prol)) (one_step l gl))) gl
 
-let out_term env = function
-  | IsConstr (c, _) -> c
-  | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr))
-
 let prolog_tac l n =
   Proofview.V82.tactic begin fun gl ->
   let map c =
     let (sigma, c) = c (pf_env gl) (project gl) in
-    let c = pf_apply (prepare_hint false (false,true)) gl (sigma, c) in
-    out_term (pf_env gl) c
+    (* Dropping the universe context is probably wrong *)
+    let (c, _) = pf_apply (prepare_hint false) gl (sigma, c) in
+    c
   in
   let l = List.map map l in
   try (prolog l n gl)
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 131832be89..ac18d5ce97 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1258,7 +1258,7 @@ let default_prepare_hint_ident = Id.of_string "H"
 
 exception Found of constr * types
 
-let prepare_hint check (poly,local) env init (sigma,c) =
+let prepare_hint check env init (sigma,c) =
   let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
   (* We re-abstract over uninstantiated evars and universes.
      It is actually a bit stupid to generalize over evars since the first
@@ -1292,10 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let empty_sigma = Evd.from_env env in
     if check then Pretyping.check_evars env empty_sigma 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 ~poly:false diff;
-	  IsConstr (c', Univ.ContextSet.empty))
+    (c', diff)
 
 let project_hint ~poly pri l2r r =
   let open EConstr in
@@ -1338,7 +1335,12 @@ let interp_hints ~poly =
     let evd,c = Constrintern.interp_open_constr env sigma c in
     let env = Global.env () in
     let sigma = Evd.from_env env in
-      prepare_hint true (poly,false) env sigma (evd,c) 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;
@@ -1419,10 +1421,8 @@ let expand_constructor_hints env sigma lems =
 		   not (Univ.ContextSet.is_empty ctx),
 		   IsConstr (mkConstructU ((ind,i+1),u),ctx))
     | _ ->
-       [match prepare_hint false (false,true) env sigma (evd,lem) with
-	| IsConstr (c, ctx) ->
-	   not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)
-	| IsGlobRef _ -> assert false (* Impossible return value *) ]) lems
+      let (c, ctx) = prepare_hint false env sigma (evd,lem) in
+      [not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 4c82a068b1..5b89f8b381 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -212,8 +212,7 @@ val interp_hints : poly:bool -> hints_expr -> hints_entry
 val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
 val prepare_hint : bool (* Check no remaining evars *) ->
-  (bool * bool) (* polymorphic or monomorphic, local or global *) ->
-  env -> evar_map -> evar_map * constr -> hint_term
+  env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
 
 (** [make_exact_entry info (c, ctyp, ctx)].
    [c] is the term given as an exact proof to solve the goal;