Typing API using EConstr.

4 files changed, 11 insertions, 11 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f4ac094b8..c2130a64a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -29,7 +29,7 @@ open Sigma.Notations
 (* Abbreviations *)
 
 let pf_env = Refiner.pf_env
-let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma c
+let pf_type_of gls c  = Typing.unsafe_type_of (pf_env gls) gls.sigma (EConstr.of_constr c)
 
 (******************************************************************)
 (* Clausal environments *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2df626e1c..93b31ced1 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -86,7 +86,7 @@ let apply_to_hyp check sign id f =
     else sign
 
 let check_typability env sigma c =
-  if !check then let _ = unsafe_type_of env sigma c in ()
+  if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
 
 (************************************************************************)
 (************************************************************************)
@@ -330,7 +330,7 @@ let meta_free_prefix sigma a =
   with Stop acc -> Array.rev_of_list acc
 
 let goal_type_of env sigma c =
-  if !check then unsafe_type_of env sigma c
+  if !check then unsafe_type_of env sigma (EConstr.of_constr c)
   else Retyping.get_type_of env sigma (EConstr.of_constr c)
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index e6e3ef47d..b62f0bea4 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -28,12 +28,12 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = NamedDecl.get_type decl in
+    let t = EConstr.of_constr (NamedDecl.get_type decl) in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
     in
     (!evdref, Environ.push_named decl env)
   in
@@ -42,12 +42,12 @@ let typecheck_evar ev env sigma =
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
   let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
+  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
   !evdref
 
 let typecheck_proof c concl env sigma =
   let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
+  let () = Typing.e_check env evdref (EConstr.of_constr c) (EConstr.of_constr concl) in
   !evdref
 
 let (pr_constrv,pr_constr) =
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b63b2ce28..148f9d675 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -93,8 +93,8 @@ let pf_nf                        = pf_reduce' simpl
 let pf_nf_betaiota               = pf_reduce' (fun _ -> nf_betaiota)
 let pf_compute                   = pf_reduce' compute
 let pf_unfoldn ubinds            = pf_reduce' (unfoldn ubinds)
-let pf_unsafe_type_of            = pf_reduce unsafe_type_of
-let pf_type_of                   = pf_reduce type_of
+let pf_unsafe_type_of            = pf_reduce' unsafe_type_of
+let pf_type_of                   = pf_reduce' type_of
 let pf_get_type_of               = pf_reduce Retyping.get_type_of
 
 let pf_conv_x gl                = pf_apply test_conversion gl Reduction.CONV
@@ -175,10 +175,10 @@ module New = struct
   let pf_concl = Proofview.Goal.concl
 
   let pf_unsafe_type_of gl t =
-    pf_apply unsafe_type_of gl t
+    pf_apply unsafe_type_of gl (EConstr.of_constr t)
 
   let pf_type_of gl t =
-    pf_apply type_of gl t
+    pf_apply type_of gl (EConstr.of_constr t)
 
   let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2