Unification API using EConstr.

5 files changed, 9 insertions, 7 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 68aeaef5e1..2d621e97cb 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -257,7 +257,7 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
   { clenv with
-      evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
+      evd = w_unify ~flags clenv.env clenv.evd cv_pb (EConstr.of_constr t1) (EConstr.of_constr t2) }
 
 let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
@@ -482,13 +482,15 @@ let error_already_defined b =
           (str "Position " ++ int n ++ str" already defined.")
 
 let clenv_unify_binding_type clenv c t u =
-  if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr u)))) then
+  let u = EConstr.of_constr u in
+  if isMeta (fst (decompose_appvect (whd_nored clenv.evd u))) then
     (* Not enough information to know if some subtyping is needed *)
     CoerceToType, clenv, c
   else
     (* Enough information so as to try a coercion now *)
     try
-      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in
+      let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd (EConstr.of_constr c) (EConstr.of_constr t) u in
+      let c = EConstr.Unsafe.to_constr c in
       TypeProcessed, { clenv with evd = evd }, c
     with 
       | PretypeError (_,_,ActualTypeNotCoercible (_,_,
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index d8a20e08bc..bc5f17bf5e 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -143,7 +143,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
     let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in
     let evd = clear_metas (Tacmach.New.project gl) in
     try
-      let evd' = w_unify env evd CONV ~flags m n in
+      let evd' = w_unify env evd CONV ~flags (EConstr.of_constr m) (EConstr.of_constr n) in
 	Proofview.Unsafe.tclEVARSADVANCE evd'
     with e when CErrors.noncritical e -> Proofview.tclZERO e
   end }
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index fd6528a1e1..4be03af9a6 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -26,7 +26,7 @@ let depends_on_evar evk _ (pbty,_,t1,t2) =
 
 let define_and_solve_constraints evk c env evd =
   if Termops.occur_evar evd evk (EConstr.of_constr c) then
-    Pretype_errors.error_occur_check env evd evk c;
+    Pretype_errors.error_occur_check env evd evk (EConstr.of_constr c);
   let evd = define evk c evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in
   match
diff --git a/proofs/goal.ml b/proofs/goal.ml
index a141708c2b..bcb14e2d6c 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -87,7 +87,7 @@ module V82 = struct
     (* Check that the goal itself does not appear in the refined term *)
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
-      else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
+      else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c)
     in
     Evd.define evk c sigma
 
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 19134bfa34..0ed74c9b36 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -98,7 +98,7 @@ let make_refine_enter ?(unsafe = true) f =
   let self = Proofview.Goal.goal gl in
   let _ =
     if not (Evarutil.occur_evar_upto sigma self c) then ()
-    else Pretype_errors.error_occur_check env sigma self c
+    else Pretype_errors.error_occur_check env sigma self (EConstr.of_constr c)
   in
   (** Proceed to the refinement *)
   let sigma = match evkmain with