Pretyping API using EConstr.

4 files changed, 8 insertions, 8 deletions

diff --git a/ltac/evar_tactics.ml b/ltac/evar_tactics.ml
index 5d3b2b886e..99023fdbbc 100644
--- a/ltac/evar_tactics.ml
+++ b/ltac/evar_tactics.ml
@@ -85,7 +85,7 @@ let let_evar name typ =
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
     | Names.Name id -> id
     in
-    let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+    let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) (EConstr.of_constr typ) in
     let tac =
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
     in
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 53b726432c..f8db0b4fcd 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -177,7 +177,7 @@ ARGUMENT EXTEND lglob
 END
 
 let interp_casted_constr ist gl c =
-  interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c
+  interp_constr_gen (Pretyping.OfType (EConstr.of_constr (pf_concl gl))) ist (pf_env gl) (project gl) c
 
 ARGUMENT EXTEND casted_constr
   TYPED AS constr
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index e1b4681975..981ff549d8 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -351,7 +351,7 @@ let refine_tac ist simple c =
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     let flags = constr_flags in
-    let expected_type = Pretyping.OfType concl in
+    let expected_type = Pretyping.OfType (EConstr.of_constr concl) in
     let c = Pretyping.type_uconstr ~flags ~expected_type ist c in
     let update = { run = fun sigma -> c.delayed env sigma } in
     let refine = Refine.refine ~unsafe:true update in
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index 58153c4534..ccd45756a6 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -95,7 +95,7 @@ let cstrevars evars = snd evars
 let new_cstr_evar (evd,cstrs) env t =
   let s = Typeclasses.set_resolvable Evd.Store.empty false in
   let evd = Sigma.Unsafe.of_evar_map evd in
-  let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in
+  let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd (EConstr.of_constr t) in
   let evd' = Sigma.to_evar_map evd' in
   let ev, _ = destEvar t in
     (evd', Evar.Set.add ev cstrs), t
@@ -1549,8 +1549,8 @@ let assert_replacing id newt tac =
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Refine.refine ~unsafe:false { run = begin fun sigma ->
-      let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
-      let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
+      let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma (EConstr.of_constr concl) in
+      let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in
       let map d =
         let n = NamedDecl.get_id d in
         if Id.equal n id then ev' else mkVar n
@@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause =
             Proofview.Goal.enter { enter = begin fun gl ->
             let env = Proofview.Goal.env gl in
             let make = { run = begin fun sigma ->
-              let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
+              let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma (EConstr.of_constr newt) in
               Sigma (mkApp (p, [| ev |]), sigma, q)
             end } in
             Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
@@ -1926,7 +1926,7 @@ let build_morphism_signature env sigma m =
   let evd = solve_constraints env !evd in
   let evd = Evd.nf_constraints evd in
   let m = Evarutil.nf_evars_universes evd morph in
-  Pretyping.check_evars env Evd.empty evd m;
+  Pretyping.check_evars env Evd.empty evd (EConstr.of_constr m);
   Evd.evar_universe_context evd, m
 
 let default_morphism sign m =