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).

12 files changed, 133 insertions, 109 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 8da30bd9c9..6fd2f7c2bc 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -238,7 +238,9 @@ let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
       raise NoChange;
     end
   in
-  let eq_constr c1 c2 = Option.has_some (Evarconv.conv env sigma c1 c2) in
+  let eq_constr c1 c2 =
+    try ignore(Evarconv.unify_delay env sigma c1 c2); true
+    with Evarconv.UnableToUnify _ -> false in
   if not (noccurn sigma 1 end_of_type)
   then nochange "dependent"; (* if end_of_type depends on this term we don't touch it  *)
     if not (isApp sigma t) then nochange "not an equality";
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 2055b25ff4..ea54973fdc 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -449,7 +449,7 @@ let evd_convertible env evd x y =
        unsolvable constraints remain, so we check that this unification
        does not introduce any new problem. *)
     let _, pbs = Evd.extract_all_conv_pbs evd in
-    let evd' = Evarconv.the_conv_x env x y evd in
+    let evd' = Evarconv.unify_delay env evd x y in
     let _, pbs' = Evd.extract_all_conv_pbs evd' in
     if evd' == evd || problem_inclusion pbs' pbs then Some evd'
     else None
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 552a4048b1..fb99b87108 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -213,7 +213,7 @@ let unif_EQ_args env sigma pa a =
   loop 0
 
 let unif_HO env ise p c =
-  try Evarconv.the_conv_x env p c ise
+  try Evarconv.unify_delay env ise p c
   with Evarconv.UnableToUnify(ise, err) ->
     raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err)))
 
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 3b904570d4..3a0e69788a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -321,9 +321,9 @@ let inh_coerce_to_ind env sigma0 loc ty tyi =
      constructor and renounce if not able to give more information *)
   (* devrait être indifférent d'exiger leq ou pas puisque pour
      un inductif cela doit être égal *)
-  match cumul env sigma expected_typ ty with
-  | Some sigma -> sigma
-  | None -> sigma0
+  match Evarconv.unify_leq_delay env sigma expected_typ ty with
+  | sigma -> sigma
+  | exception Evarconv.UnableToUnify _ -> sigma0
 
 let binding_vars_of_inductive sigma = function
   | NotInd _ -> []
@@ -431,9 +431,9 @@ let adjust_tomatch_to_pattern ~program_mode sigma pb ((current,typ),deps,dep) =
             let sigma, current =
               if List.is_empty deps && isEvar sigma typ then
 	      (* Don't insert coercions if dependent; only solve evars *)
-                match cumul !!(pb.env) sigma indt typ with
-                | None -> sigma, current
-                | Some sigma -> sigma, current
+                match Evarconv.unify_leq_delay !!(pb.env) sigma indt typ with
+                | exception Evarconv.UnableToUnify _ -> sigma, current
+                | sigma -> sigma, current
 	      else
                 let sigma, j = Coercion.inh_conv_coerce_to ~program_mode true !!(pb.env) sigma (make_judge current typ) indt in
                 sigma, j.uj_val
@@ -1767,9 +1767,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t =
         let sigma, t = abstract_tycon ?loc tycon_env sigma subst tycon extenv t in
         let sigma, tt = Typing.type_of !!extenv sigma t in
         (sigma, t, tt) in
-  match cumul !!env sigma tt (mkSort s) with
-  | None -> anomaly (Pp.str "Build_tycon: should be a type.");
-  | Some sigma ->
+  match unify_leq_delay !!env sigma tt (mkSort s) with
+  | exception Evarconv.UnableToUnify _ -> anomaly (Pp.str "Build_tycon: should be a type.");
+  | sigma ->
     sigma, { uj_val = t; uj_type = tt }
 
 (* For a multiple pattern-matching problem Xi on t1..tn with return
@@ -2190,15 +2190,15 @@ let constr_of_pat env sigma arsign pat avoid =
                 let sigma, sign, i, avoid =
 		  try
                     let env = EConstr.push_rel_context sign env in
-                    let sigma = the_conv_x_leq (EConstr.push_rel_context sign env)
-                      (lift (succ m) ty) (lift 1 apptype) sigma in
+                    let sigma = unify_leq_delay (EConstr.push_rel_context sign env) sigma
+                      (lift (succ m) ty) (lift 1 apptype) in
                     let sigma, eq_t = mk_eq sigma (lift (succ m) ty)
 		      (mkRel 1) (* alias *)
 		      (lift 1 app) (* aliased term *)
 		    in
 		    let neq = eq_id avoid id in
                       sigma, LocalDef (Name neq, mkRel 0, eq_t) :: sign, 2, Id.Set.add neq avoid
-                  with Reduction.NotConvertible -> sigma, sign, 1, avoid
+                  with Evarconv.UnableToUnify _ -> sigma, sign, 1, avoid
 		in
 		  (* Mark the equality as a hole *)
                   sigma, pat', sign, lift i app, lift i apptype, realargs, n + i, avoid
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index a8bcec10e8..0adf9365cf 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -64,9 +64,9 @@ let apply_coercion_args env sigma check isproj argl funj =
       | Prod (_,c1,c2) ->
         let sigma =
           if check then
-            begin match cumul env sigma (Retyping.get_type_of env sigma h) c1 with
-              | None -> raise NoCoercion
-              | Some sigma -> sigma
+            begin match Evarconv.unify_leq_delay env sigma (Retyping.get_type_of env sigma h) c1 with
+              | exception Evarconv.UnableToUnify _ -> raise NoCoercion
+              | sigma -> sigma
             end
           else sigma
         in
@@ -157,7 +157,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
   let rec coerce_unify env x y =
     let x = hnf env !evdref x and y = hnf env !evdref y in
       try
-	evdref := the_conv_x_leq env x y !evdref;
+        evdref := Evarconv.unify_leq_delay env !evdref x y;
 	None
       with UnableToUnify _ -> coerce' env x y
   and coerce' env x y : (EConstr.constr -> EConstr.constr) option =
@@ -172,7 +172,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
       let rec aux tele typ typ' i co =
 	if i < len then
 	  let hdx = l.(i) and hdy = l'.(i) in
-	    try evdref := the_conv_x_leq env hdx hdy !evdref;
+            try evdref := unify_leq_delay env !evdref hdx hdy;
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
@@ -180,8 +180,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	      let (n, eqT), restT = dest_prod typ in
 	      let (n', eqT'), restT' = dest_prod typ' in
               let () =
-		try evdref := the_conv_x_leq env eqT eqT' !evdref
-		with UnableToUnify _ -> raise NoSubtacCoercion
+                try evdref := unify_leq_delay env !evdref eqT eqT'
+                with UnableToUnify _ -> raise NoSubtacCoercion
 	      in
 		(* Disallow equalities on arities *)
 		if Reductionops.is_arity env !evdref eqT then raise NoSubtacCoercion;
@@ -483,14 +483,14 @@ let inh_coerce_to_fail flags env evd rigidonly v t c1 =
 	  | None -> evd, None, t
       with Not_found -> raise NoCoercion
     in
-      try (unify_leq flags env evd t' c1, v')
+      try (unify_leq_delay ~flags env evd t' c1, v')
       with UnableToUnify _ -> raise NoCoercion
 
 let default_flags_of env =
   default_flags_of TransparentState.full
 
 let rec inh_conv_coerce_to_fail ?loc env evd ?(flags=default_flags_of env) rigidonly v t c1 =
-  try (unify_leq flags env evd t c1, v)
+  try (unify_leq_delay ~flags env evd t c1, v)
   with UnableToUnify (best_failed_evd,e) ->
     try inh_coerce_to_fail flags env evd rigidonly v t c1
     with NoCoercion ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28dd63cfcc..dc613640d7 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1720,44 +1720,48 @@ let solve_unif_constraints_with_heuristics env
 
 exception UnableToUnify of evar_map * unification_error
 
-let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
-  match evar_conv_x flags env evd CONV  t1 t2 with
+let unify_delay ?flags env evd t1 t2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
+  match evar_conv_x flags env evd CONV t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
-let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
-  let flags = default_flags_of ts in
+let unify_leq_delay ?flags env evd t1 t2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
   match evar_conv_x flags env evd CUMUL t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
-let make_opt = function
-  | Success evd -> Some evd
-  | UnifFailure _ -> None
-
-let conv env ?(ts=default_transparent_state env) evd t1 t2 =
-  let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CONV t1 t2)
+let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 =
+  let flags =
+    match flags with
+    | None -> default_flags_of (default_transparent_state env)
+    | Some flags -> flags
+  in
+  let res = evar_conv_x flags env evd cv_pb ty1 ty2 in
+  match res with
+  | Success evd ->
+     solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
+  | UnifFailure (evd, reason) ->
+     raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))
 
-let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
+(* deprecated *)
+let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
   let flags = default_flags_of ts in
-  make_opt(evar_conv_x flags env evd CUMUL t1 t2)
-
-let unify flags env evd t1 t2 =
-  match evar_conv_x flags env evd CONV t1 t2 with
+  match evar_conv_x flags env evd CONV  t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
 
-let unify_leq flags env evd t1 t2 =
+let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
+  let flags = default_flags_of ts in
   match evar_conv_x flags env evd CUMUL t1 t2 with
   | Success evd' -> evd'
   | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
-
-let unify_with_heuristics flags ~with_ho env evd cv_pb ty1 ty2 =
-  let res = evar_conv_x flags env evd cv_pb ty1 ty2 in
-  match res with
-  | Success evd ->
-     solve_unif_constraints_with_heuristics ~flags ~with_ho env evd
-  | UnifFailure (evd, reason) ->
-     raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason)))
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index fa6f3466f6..0418b352fe 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -30,34 +30,50 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
 
 (** {6 Main unification algorithm for type inference. } *)
 
-(** returns exception NotUnifiable with best known evar_map if not unifiable *)
+(** There are two variants for unification: one that delays constraints outside its capabilities
+    ([unify_delay]) and another that tries to solve such remaining constraints using
+    heuristics ([unify]). *)
+
+(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints.
+    In case of success, the two terms are hence unifiable only if the remaining constraints
+    can be solved or [check_problems_are_solved] is true.
+
+    @raises UnableToUnify in case the two terms do not unify *)
+
+val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
+val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map
+
+(** returns exception UnableToUnify with best known evar_map if not unifiable *)
 val the_conv_x     : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
+[@@ocaml.deprecated "Use Evarconv.unify_delay instead"]
 val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
+[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"]
 
-(** Allows to pass arbitrary flags to the unifier *)
-val unify : unify_flags -> env -> evar_map -> constr -> constr -> evar_map
-val unify_leq : unify_flags -> env -> evar_map -> constr -> constr -> evar_map
+(** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining
+    constraints. In case of success the two terms are unified without condition.
 
-(** @raises a PretypeError if it cannot unify *)
-val unify_with_heuristics : unify_flags -> with_ho:bool ->
-                            env -> evar_map -> conv_pb -> constr -> constr -> evar_map
-
-(** The same function resolving evars by side-effect and
-   catching the exception *)
-val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
-val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
+    The with_ho option tells if higher-order unification should be tried to resolve the
+    constraints.
 
+    @raises a PretypeError if it cannot unify *)
+val unify : ?flags:unify_flags -> ?with_ho:bool ->
+  env -> evar_map -> conv_pb -> constr -> constr -> evar_map
 
 (** {6 Unification heuristics. } *)
 
 (** Try heuristics to solve pending unification problems and to solve
-    evars with candidates *)
+   evars with candidates.
+
+   The with_ho option tells if higher-order unification should be tried
+   to resolve the constraints.
+
+    @raises a PretypeError if it fails to resolve some problem *)
 
 val solve_unif_constraints_with_heuristics :
   env -> ?flags:unify_flags -> ?with_ho:bool -> evar_map -> evar_map
 
-(** Check all pending unification problems are solved and raise an
-    error otherwise *)
+(** Check all pending unification problems are solved and raise a
+    PretypeError otherwise *)
 
 val check_problems_are_solved : env -> evar_map -> unit
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e65bdd8220..770dfe328f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -556,9 +556,9 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
 	  | GFix (vn,i) -> i
 	  | GCoFix i -> i
         in
-        begin match conv !!env sigma ftys.(fixi) t with
-          | None -> sigma
-          | Some sigma -> sigma
+        begin match Evarconv.unify_delay !!env sigma ftys.(fixi) t with
+          | exception Evarconv.UnableToUnify _ -> sigma
+          | sigma -> sigma
         end
       | None -> sigma
     in
@@ -667,11 +667,11 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
             match candargs with
             | [] -> sigma, [], j_val hj
             | arg :: args ->
-              begin match conv !!env sigma (j_val hj) arg with
-                | Some sigma ->
-                  sigma, args, nf_evar sigma (j_val hj)
-                | None ->
+              begin match Evarconv.unify_delay !!env sigma (j_val hj) arg with
+                | exception Evarconv.UnableToUnify _ ->
                   sigma, [], j_val hj
+                | sigma ->
+                  sigma, args, nf_evar sigma (j_val hj)
               end
           in
             let sigma, ujval = adjust_evar_source sigma na ujval in
@@ -1057,9 +1057,9 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
 	match valcon with
         | None -> sigma, tj
 	| Some v ->
-          begin match cumul !!env sigma v tj.utj_val with
-            | Some sigma -> sigma, tj
-            | None ->
+          begin match Evarconv.unify_leq_delay !!env sigma v tj.utj_val with
+            | sigma -> sigma, tj
+            | exception Evarconv.UnableToUnify _ ->
 	      error_unexpected_type
                 ?loc:(loc_of_glob_constr c) !!env sigma tj.utj_val v
           end
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index e8d935fcbb..0b54160b3f 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -71,10 +71,10 @@ let judge_of_applied_inductive_knowing_parameters env sigma funj ind argjv =
          | _ ->
              error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env sigma hj.uj_type c1 with
-         | Some sigma ->
+       begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with
+         | sigma ->
            apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
-         | None ->
+         | exception Evarconv.UnableToUnify _ ->
            error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
@@ -96,10 +96,10 @@ let judge_of_apply env sigma funj argjv =
          | _ ->
             error_cant_apply_not_functional env sigma funj argjv
        in
-       begin match Evarconv.cumul env sigma hj.uj_type c1 with
-         | Some sigma ->
+       begin match Evarconv.unify_leq_delay env sigma hj.uj_type c1 with
+         | sigma ->
            apply_rec sigma (n+1) (subst1 hj.uj_val c2) restjl
-         | None ->
+         | exception Evarconv.UnableToUnify _ ->
            error_cant_apply_bad_type env sigma (n, c1, hj.uj_type) funj argjv
        end
   in
@@ -109,9 +109,9 @@ let check_branch_types env sigma (ind,u) cj (lfj,explft) =
   if not (Int.equal (Array.length lfj) (Array.length explft)) then
     error_number_branches env sigma cj (Array.length explft);
   Array.fold_left2_i (fun i sigma lfj explft ->
-      match Evarconv.cumul env sigma lfj.uj_type explft with
-      | Some sigma -> sigma
-      | None ->
+      match Evarconv.unify_leq_delay env sigma lfj.uj_type explft with
+      | sigma -> sigma
+      | exception Evarconv.UnableToUnify _ ->
         error_ill_formed_branch env sigma cj.uj_val ((ind,i+1),u) lfj.uj_type explft)
     sigma lfj explft
 
@@ -127,9 +127,9 @@ let is_correct_arity env sigma c pj ind specif params =
     let pt' = whd_all env sigma pt in
     match EConstr.kind sigma pt', ar with
     | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' ->
-      begin match Evarconv.cumul env sigma a1 a1' with
-        | None -> error ()
-        | Some sigma ->
+      begin match Evarconv.unify_leq_delay env sigma a1 a1' with
+        | exception Evarconv.UnableToUnify _ -> error ()
+        | sigma ->
           srec (push_rel (LocalAssum (na1,a1)) env) sigma t ar'
       end
     | Sort s, [] ->
@@ -187,9 +187,9 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
   let lt = Array.length vdefj in
   assert (Int.equal (Array.length lar) lt);
   Array.fold_left2_i (fun i sigma defj ar ->
-      match Evarconv.cumul env sigma defj.uj_type (lift lt ar) with
-      | Some sigma -> sigma
-      | None ->
+      match Evarconv.unify_leq_delay env sigma defj.uj_type (lift lt ar) with
+      | sigma -> sigma
+      | exception Evarconv.UnableToUnify _ ->
         error_ill_typed_rec_body ?loc env sigma
           i lna vdefj lar)
     sigma vdefj lar
@@ -211,10 +211,10 @@ let check_allowed_sort env sigma ind c p =
 
 let judge_of_cast env sigma cj k tj =
   let expected_type = tj.utj_val in
-  match Evarconv.cumul env sigma cj.uj_type expected_type with
-  | None ->
+  match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with
+  | exception Evarconv.UnableToUnify _ ->
     error_actual_type_core env sigma cj expected_type;
-  | Some sigma ->
+  | sigma ->
     sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
              uj_type = expected_type }
 
@@ -427,10 +427,10 @@ and execute_array env = Array.fold_left_map (execute env)
 
 let check env sigma c t =
   let sigma, j = execute env sigma c in
-  match Evarconv.cumul env sigma j.uj_type t with
-  | None ->
+  match Evarconv.unify_leq_delay env sigma j.uj_type t with
+  | exception Evarconv.UnableToUnify _ ->
     error_actual_type_core env sigma j t
-  | Some sigma -> sigma
+  | sigma -> sigma
 
 (* Type of a constr *)
 
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 *)