Remove all uses of clenv_unique_resolver.

All calls to this function are now factorized through Clenvtac.res_pf.

6 files changed, 7 insertions, 23 deletions

diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 6eafca359b..a34ec0e5be 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -16,7 +16,6 @@ open Unification
 
 (** Tactics *)
 val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic
-val clenv_refine : ?with_evars:bool -> ?with_classes:bool -> clausenv -> unit Proofview.tactic
 val res_pf : ?with_evars:bool -> ?with_classes:bool -> ?flags:unify_flags -> clausenv -> unit Proofview.tactic
 
 val clenv_pose_dependent_evars : ?with_evars:bool -> clausenv -> clausenv
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f041af1db1..4f7bb7ee1e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -99,8 +99,7 @@ let connect_hint_clenv h gl =
 let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
   let clenv, c = connect_hint_clenv h gl in
-  let clenv = clenv_unique_resolver ~flags clenv gl in
-  Clenvtac.clenv_refine clenv
+  Clenvtac.res_pf ~flags clenv
   end
 
 let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 484aab2f00..56d6f7f09a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -14,7 +14,6 @@
  *)
 
 open Pp
-open CErrors
 open Util
 open Names
 open Term
@@ -162,24 +161,14 @@ let e_give_exact flags h =
   Clenvtac.unify ~flags t1 <*> exact_no_check c
   end
 
-let clenv_unique_resolver_tac with_evars ~flags clenv' =
-  Proofview.Goal.enter begin fun gls ->
-    let resolve =
-      try Proofview.tclUNIT (clenv_unique_resolver ~flags clenv' gls)
-      with e when noncritical e ->
-        let _, info = Exninfo.capture e in
-        Proofview.tclZERO ~info e
-    in resolve >>= fun clenv' ->
-       Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
-  end
-
 let unify_e_resolve flags = begin fun gls (h, _) ->
   let clenv', c = connect_hint_clenv h gls in
-  clenv_unique_resolver_tac true ~flags clenv' end
+  Clenvtac.res_pf ~with_evars:true ~with_classes:false ~flags clenv'
+  end
 
 let unify_resolve flags = begin fun gls (h, _) ->
   let clenv', _ = connect_hint_clenv h gls in
-  clenv_unique_resolver_tac false ~flags clenv'
+  Clenvtac.res_pf ~with_evars:false ~with_classes:false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 90e4aaa167..7269228485 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -68,8 +68,7 @@ open Auto
 let unify_e_resolve flags h =
   Proofview.Goal.enter begin fun gl ->
       let clenv', c = connect_hint_clenv h gl in
-      let clenv' = clenv_unique_resolver ~flags clenv' gl in
-      Clenvtac.clenv_refine ~with_evars:true ~with_classes:true clenv'
+      Clenvtac.res_pf ~with_evars:true ~with_classes:true ~flags clenv'
     end
 
 let hintmap_of sigma secvars concl =
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index af10a2fae5..483d8a726b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -684,7 +684,6 @@ module New = struct
       | None   -> elimclause'
       | Some p -> clenv_unify ~flags Reduction.CONV (mkMeta pmv) p elimclause'
     in
-    let clenv' = clenv_unique_resolver ~flags elimclause' gl in
     let after_tac i =
       let ba = { branchsign = branchsigns.(i);
                  branchnames = brnames.(i);
@@ -696,7 +695,7 @@ module New = struct
     in
     let branchtacs = List.init (Array.length branchsigns) after_tac in
     Proofview.tclTHEN
-      (Clenvtac.clenv_refine clenv')
+      (Clenvtac.res_pf ~flags elimclause')
       (Proofview.tclEXTEND [] tclIDTAC branchtacs)
     end) end
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 65f79b6a51..fd9fd81500 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4371,8 +4371,7 @@ let induction_tac with_evars params indvars elim =
   (* elimclause' is built from elimclause by instantiating all args and params. *)
   let elimclause' = recolle_clenv i params indvars elimclause gl in
   (* one last resolution (useless?) *)
-  let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
-  Clenvtac.clenv_refine ~with_evars resolved
+  Clenvtac.res_pf ~with_evars ~flags:(elim_flags ()) elimclause'
   end
 
 (* Apply induction "in place" taking into account dependent