[api] Remove `polymorphic` type alias, use labels instead.

This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)

1 files changed, 9 insertions, 9 deletions

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)