Pretyping API using EConstr.

5 files changed, 6 insertions, 6 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0515e41986..68aeaef5e1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -337,7 +337,7 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = Sigma.Unsafe.of_evar_map clenv.evd in
-	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
+	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src (EConstr.of_constr ty) in
 	let evd = Sigma.to_evar_map evd in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
@@ -610,7 +610,7 @@ let make_evar_clause env sigma ?len t =
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
       let sigma = Sigma.Unsafe.of_evar_map sigma in
-      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
+      let Sigma (ev, sigma, _) = new_evar ~store env sigma (EConstr.of_constr t1) in
       let sigma = Sigma.to_evar_map sigma in
       let dep = not (EConstr.Vars.noccurn sigma 1 (EConstr.of_constr t2)) in
       let hole = {
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index af5fa921f7..fd6528a1e1 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -51,7 +51,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
+      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err ~loc 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 93b31ced16..093d949d5d 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -314,7 +314,7 @@ let check_meta_variables c =
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check then
-    let evm, b = Reductionops.infer_conv env sigma ty conclty in
+    let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
       if b then evm 
       else raise (RefinerError (BadType (arg,ty,conclty)))
   else sigma
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 67e216745d..af910810ba 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -236,6 +236,6 @@ let solve_by_implicit_tactic env sigma evk =
         let (ans, _, ctx) =
 	  build_by_tactic env (Evd.evar_universe_context sigma) c tac in
         let sigma = Evd.set_universe_context sigma ctx in
-        sigma, ans
+        sigma, EConstr.of_constr ans
        with e when Logic.catchable_exception e -> raise Exit)
   | _ -> raise Exit
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 7458109fa1..807a554dfd 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -190,4 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit
 val clear_implicit_tactic : unit -> unit
 
 (* Raise Exit if cannot solve *)
-val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr
+val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * EConstr.constr