Retyping API using EConstr.

4 files changed, 15 insertions, 15 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 6ca34036a..42a8cac69 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -42,11 +42,11 @@ let none = Evd.empty
 
 let type_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
+  Retyping.get_type_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c)))
 
 let sort_of env c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c))
+  Retyping.get_sort_family_of ~polyprop env none (EConstr.of_constr (strip_outer_cast none (EConstr.of_constr c)))
 
 (*S Generation of flags and signatures. *)
 
@@ -595,7 +595,7 @@ let rec extract_term env mle mlt c args =
     | Construct (cp,_) ->
 	extract_cons_app env mle mlt cp args
     | Proj (p, c) ->
-        let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
+        let term = Retyping.expand_projection env (Evd.from_env env) p (EConstr.of_constr c) [] in
 	  extract_term env mle mlt term args
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 9fb1463db..a943ef2b0 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1199,7 +1199,7 @@ struct
       with e when CErrors.noncritical e -> (X(t),env,tg) in
 
     let is_prop term =
-      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) term in 
+      let sort  = Retyping.get_sort_of (Tacmach.pf_env gl)  (Tacmach.project gl) (EConstr.of_constr term) in 
      Term.is_prop_sort sort in
      
     let rec xparse_formula env tg term =
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index b129b0bb3..f88b3a700 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -94,9 +94,9 @@ let rec make_form atom_env gls term =
   let cciterm=special_whd gls term  in
     match kind_of_term cciterm with
 	Prod(_,a,b) ->
-	  if EConstr.Vars.noccurn Evd.empty (** FIXME *) 1 (EConstr.of_constr b) &&
+	  if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) &&
 	    Retyping.get_sort_family_of
-	    (pf_env gls) (Tacmach.project gls) a == InProp
+	    (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp
 	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
@@ -136,7 +136,7 @@ let rec make_hyps atom_env gls lenv = function
 	make_hyps atom_env gls (typ::lenv) rest in
 	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv ||
 	  (Retyping.get_sort_family_of
-	     (pf_env gls) (Tacmach.project gls) typ != InProp)
+	     (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp)
 	then
 	  hrec
 	else
@@ -262,7 +262,7 @@ let rtauto_tac gls=
   let gl=pf_concl gls in
   let _=
     if Retyping.get_sort_family_of
-      (pf_env gls) (Tacmach.project gls) gl != InProp
+      (pf_env gls) (Tacmach.project gls) (EConstr.of_constr gl) != InProp
     then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index cf0f51911..e1b95ddbc 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -345,9 +345,9 @@ let ring_for_carrier r = Cmap.find r !from_carrier
 let find_ring_structure env sigma l =
   match l with
     | t::cl' ->
-        let ty = Retyping.get_type_of env sigma t in
+        let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in
         let check c =
-          let ty' = Retyping.get_type_of env sigma c in
+          let ty' = Retyping.get_type_of env sigma (EConstr.of_constr c) in
           if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
             user_err ~hdr:"ring"
               (str"arguments of ring_simplify do not have all the same type")
@@ -540,7 +540,7 @@ let build_setoid_params env evd r add mul opp req eqth =
     | None -> ring_equality env evd (r,add,mul,opp,req)
 
 let dest_ring env sigma th_spec =
-  let th_typ = Retyping.get_type_of env sigma th_spec in
+  let th_typ = Retyping.get_type_of env sigma (EConstr.of_constr th_spec) in
   match kind_of_term th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
         when eq_constr_nounivs f (Lazy.force coq_almost_ring_theory) ->
@@ -571,7 +571,7 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
               TacArg(Loc.ghost,TacCall(Loc.ghost,t,[]))
 
 let make_hyp env evd c =
-  let t = Retyping.get_type_of env !evd c in
+  let t = Retyping.get_type_of env !evd (EConstr.of_constr c) in
    plapp evd coq_mkhypo [|t;c|]
 
 let make_hyp_list env evd lH =
@@ -796,7 +796,7 @@ let af_ar = my_reference"AF_AR"
 let f_r = my_reference"F_R"
 let sf_sr = my_reference"SF_SR"
 let dest_field env evd th_spec =
-  let th_typ = Retyping.get_type_of env !evd th_spec in
+  let th_typ = Retyping.get_type_of env !evd (EConstr.of_constr th_spec) in
   match kind_of_term th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
         when is_global (Lazy.force afield_theory) f ->
@@ -825,9 +825,9 @@ let find_field_structure env sigma l =
   check_required_library (cdir@["Field_tac"]);
   match l with
     | t::cl' ->
-        let ty = Retyping.get_type_of env sigma t in
+        let ty = Retyping.get_type_of env sigma (EConstr.of_constr t) in
         let check c =
-          let ty' = Retyping.get_type_of env sigma c in
+          let ty' = Retyping.get_type_of env sigma (EConstr.of_constr c) in
           if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
             user_err ~hdr:"field"
               (str"arguments of field_simplify do not have all the same type")