Move the hint polymorphic status to the hint instance.

It is only used for this kind of hints, never for Extern / Unfold.

1 files changed, 13 insertions, 14 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4ed01d4e65..f041af1db1 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 h gl =
+let connect_hint_clenv h gl =
   let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
   (* [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
@@ -78,7 +78,7 @@ let connect_hint_clenv ~poly h gl =
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (* Still, we need to update the universes *)
   let clenv, c =
-    if poly then
+    if h.hint_poly then
       (* Refresh the instance of the hint *)
       let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
@@ -96,22 +96,22 @@ let connect_hint_clenv ~poly h gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve ~poly flags (h : hint) =
+let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv ~poly h gl in
+  let clenv, c = connect_hint_clenv h 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 h = unify_resolve auto_unif_flags h
 
-let unify_resolve_gen ~poly = function
-  | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve ~poly flags
+let unify_resolve_gen = function
+  | None -> unify_resolve_nodelta
+  | Some flags -> unify_resolve flags
 
-let exact poly h =
+let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly h gl in
+    let clenv', c = connect_hint_clenv h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -383,16 +383,15 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
         (local_db::db_list)
 
 and tac_of_hint dbg db_list local_db concl (flags, h) =
-  let poly = FullHint.is_polymorphic h in
   let tactic = function
-    | Res_pf h -> unify_resolve_gen ~poly flags h
+    | Res_pf h -> unify_resolve_gen flags h
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
         let info = Exninfo.reify () in
         Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
-    | Give_exact h  -> exact poly h
+    | Give_exact h  -> exact h
     | Res_pf_THEN_trivial_fail h ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen ~poly flags h)
+        (unify_resolve_gen flags h)
         (* 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)