Change interfaces of evarconv as suggested by Enrico.

Now the main functions are unify (solves the problems entirely) and
unify_delay and unify_leq (which might leave some unsolved constraints).

Deprecated the_conv_x and the_conv_x_leq (which were misnommers as they
do unification not conversion).

3 files changed, 15 insertions, 13 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 429bada7e3..d770d0614a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -230,8 +230,9 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
       let sigma', cl = Clenv.make_evar_clause env sigma ?len:n ty in
       let term = applist (term, List.map (fun x -> x.hole_evar) cl.cl_holes) in
       let sigma' =
-        Evarconv.the_conv_x_leq env ~ts:flags.core_unify_flags.modulo_delta
-                                cl.cl_concl concl sigma'
+        Evarconv.(unify_leq_delay
+                    ~flags:(default_flags_of flags.core_unify_flags.modulo_delta)
+                              env sigma' cl.cl_concl concl)
       in (sigma', term) end
 
 let unify_resolve_refine poly flags gl clenv =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a8cfc87f9c..4a1bb37fa4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -636,7 +636,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
   let evd = 
     if unsafe then Some (Tacmach.New.project gl)
     else
-      try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
+      try Some (Evarconv.unify_delay (Proofview.Goal.env gl) (Tacmach.New.project gl) t1 t2)
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -1194,9 +1194,8 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       (* is the default value typable with the expected type *)
       let dflt_typ = unsafe_type_of env sigma dflt in
       try
-        let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
-        let sigma =
-          Evarconv.solve_unif_constraints_with_heuristics env sigma in
+        let sigma = Evarconv.unify_leq_delay env sigma dflt_typ p_i in
+        let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in
         sigma, dflt
       with Evarconv.UnableToUnify _ ->
 	user_err Pp.(str "Cannot solve a unification problem.")
@@ -1211,11 +1210,11 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       match evopt with
 	| Some w ->
           let w_type = unsafe_type_of env sigma w in
-          begin match Evarconv.cumul env sigma w_type a with
-            | Some sigma ->
+          begin match Evarconv.unify_leq_delay env sigma w_type a with
+            | sigma ->
               let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
               sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
-            | None ->
+            | exception Evarconv.UnableToUnify _ ->
               user_err Pp.(str "Cannot solve a unification problem.")
           end
 	| None ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index db59f7cfc2..415225454a 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3840,9 +3840,9 @@ let specialize_eqs id =
   let evars = ref (Proofview.Goal.sigma gl) in
   let unif env evars c1 c2 =
     compare_upto_variables !evars c1 c2 &&
-    (match Evarconv.conv env !evars c1 c2 with
-     | Some sigma -> evars := sigma; true
-     | None -> false)
+    (match Evarconv.unify_delay env !evars c1 c2 with
+     | sigma -> evars := sigma; true
+     | exception Evarconv.UnableToUnify _ -> false)
   in
   let rec aux in_eqs ctx acc ty =
     match EConstr.kind !evars ty with
@@ -4398,7 +4398,9 @@ let check_expected_type env sigma (elimc,bl) elimt =
   let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in
   let sigma = solve_evar_clause env sigma true cl bl in
   let (_,u,_) = destProd sigma cl.cl_concl in
-  fun t -> Option.has_some (Evarconv.cumul env sigma t u)
+  fun t -> match Evarconv.unify_leq_delay env sigma t u with
+    | _sigma -> true
+    | exception Evarconv.UnableToUnify _ -> false
 
 let check_enough_applied env sigma elim =
   (* A heuristic to decide whether the induction arg is enough applied *)