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, 8 insertions, 9 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 4a6364795b..0ff90bc046 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -65,9 +65,9 @@ open Auto
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let unify_e_resolve poly flags h =
+let unify_e_resolve flags 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
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl =
      else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
-let e_exact poly flags h =
+let e_exact flags 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))
     (e_give_exact c)
@@ -121,17 +121,16 @@ and e_my_find_search env sigma db_list local_db secvars concl =
   in
   let tac_of_hint =
     fun (st, h) ->
-      let poly = FullHint.is_polymorphic h in
       let b = match FullHint.repr h with
       | Unfold_nth _ -> 1
       | _ -> FullHint.priority h
       in
       let tac = function
-      | Res_pf h -> unify_resolve ~poly st h
-      | ERes_pf h -> unify_e_resolve poly st h
-      | Give_exact h -> e_exact poly st h
+      | Res_pf h -> unify_resolve st h
+      | ERes_pf h -> unify_e_resolve st h
+      | Give_exact h -> e_exact st h
       | Res_pf_THEN_trivial_fail h ->
-        Tacticals.New.tclTHEN (unify_e_resolve poly st h)
+        Tacticals.New.tclTHEN (unify_e_resolve st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
       | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast