Evarconv API using EConstr.

3 files changed, 7 insertions, 7 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 6fb90e7af..a31e581e8 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -264,7 +264,7 @@ let unify_resolve_refine poly flags =
       let sigma' =
         let evdref = ref sigma' in
         if not (Evarconv.e_cumul env ~ts:flags.core_unify_flags.modulo_delta
-                                      evdref cl.cl_concl concl) then
+                                      evdref (EConstr.of_constr cl.cl_concl) (EConstr.of_constr concl)) then
           Type_errors.error_actual_type env
             {Environ.uj_val = term; Environ.uj_type = cl.cl_concl}
             concl;
@@ -1506,7 +1506,7 @@ let not_evar c =
   | _ -> Proofview.tclUNIT ()
 
 let is_ground c gl =
-  if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
+  if Evarutil.is_ground_term (project gl) (EConstr.of_constr c) then tclIDTAC gl
   else tclFAIL 0 (str"Not ground") gl
 
 let autoapply c i gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e87746a28..17038e42d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -626,7 +626,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.the_conv_x (Proofview.Goal.env gl) (EConstr.of_constr t1) (EConstr.of_constr t2) (Tacmach.New.project gl))
       with Evarconv.UnableToUnify _ -> None
   in
   match evd with
@@ -1167,7 +1167,7 @@ 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 () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
+	let () = evdref := Evarconv.the_conv_x_leq env (EConstr.of_constr dflt_typ) (EConstr.of_constr p_i) !evdref in
 	let () = evdref := Evarconv.consider_remaining_unif_problems env !evdref in
 	dflt
       with Evarconv.UnableToUnify _ ->
@@ -1185,7 +1185,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
       with
 	| Some w ->
             let w_type = unsafe_type_of env sigma w in
-            if Evarconv.e_cumul env evdref w_type a then
+            if Evarconv.e_cumul env evdref (EConstr.of_constr w_type) (EConstr.of_constr a) then
 	      let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 1c10cdfea..c2163a274 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3731,7 +3731,7 @@ let specialize_eqs id gl =
   let ty = Tacmach.pf_get_hyp_typ gl id in
   let evars = ref (project gl) in
   let unif env evars c1 c2 =
-    compare_upto_variables c1 c2 && Evarconv.e_conv env evars c1 c2
+    compare_upto_variables c1 c2 && Evarconv.e_conv env evars (EConstr.of_constr c1) (EConstr.of_constr c2)
   in
   let rec aux in_eqs ctx acc ty =
     match kind_of_term ty with
@@ -4275,7 +4275,7 @@ 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 cl.cl_concl in
-  fun t -> Evarconv.e_cumul env (ref sigma) t u
+  fun t -> Evarconv.e_cumul env (ref sigma) (EConstr.of_constr t) (EConstr.of_constr u)
 
 let check_enough_applied env sigma elim =
   let sigma = Sigma.to_evar_map sigma in