Removing compatibility layers in Retyping

9 files changed, 17 insertions, 17 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7a99c45a8..a4ed4798a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -264,7 +264,6 @@ let refresh_universes ty k =
     let env = Proofview.Goal.env gl in
     let evm = Tacmach.New.project gl in
     let evm, ty = refresh_type env evm ty in
-    let ty = EConstr.of_constr ty in
     Sigma.Unsafe.of_pair (k ty, evm)
   end }
 
@@ -387,7 +386,6 @@ let discriminate_tac (cstr,u as cstru) p =
     let trivial = EConstr.of_constr trivial in
     let evm = Tacmach.New.project gl in
     let evm, intype = refresh_type env evm (EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl t1)) in
-    let intype = EConstr.of_constr intype in
     let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in
     let outtype = mkSort outtype in
     let pred = mkLambda(Name xid,outtype,mkRel 1) in
@@ -496,9 +494,7 @@ let mk_eq f c1 c2 k =
   Proofview.Goal.enter { enter = begin fun gl ->
     let open Tacmach.New in
     let evm, ty = pf_apply type_of gl c1 in
-    let ty = EConstr.of_constr ty in
     let evm, ty = Evarsolve.refresh_universes (Some false) (pf_env gl) evm ty in
-    let ty = EConstr.of_constr ty in
     let term = mkApp (fc, [| ty; c1; c2 |]) in
     let evm, _ =  type_of (pf_env gl) evm term in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm))
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 61547f96d..7b7e746f2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -42,7 +42,7 @@ 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))
+  EConstr.Unsafe.to_constr (Retyping.get_type_of ~polyprop env none (strip_outer_cast none (EConstr.of_constr c)))
 
 let sort_of env c =
   let polyprop = (lang() == Haskell) in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index cc29d68f5..c98cdc467 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -985,6 +985,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let (type_ctxt,type_of_f),evd =
     let evd,t = Typing.type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f)
     in 
+    let t = EConstr.Unsafe.to_constr t in
     decompose_prod_n_assum
       (nb_params + nb_args) t,evd
   in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 38cd21684..0725bb11c 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1273,6 +1273,7 @@ let do_build_inductive
     Array.fold_right2
       (fun id c (evd,env) ->
        let evd,t = Typing.type_of env evd (EConstr.mkConstU c) in
+       let t = EConstr.Unsafe.to_constr t in
        evd,
        Environ.push_named (LocalAssum (id,t))
 			   (* try *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 37a76bec1..1b899c152 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -373,6 +373,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
 	     let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
+	     let princ_type = EConstr.Unsafe.to_constr princ_type in
     	     Functional_principles_types.generate_functional_principle
 	       evd
 		 interactive_proof
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ca066c4cc..27528c2dc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -135,6 +135,7 @@ let generate_type evd g_to_f f graph i =
   in
   evd:=evd';
   let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
+  let graph_arity = EConstr.Unsafe.to_constr graph_arity in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -203,6 +204,7 @@ let find_induction_principle evd f =
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
        let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
+       let typ = EConstr.Unsafe.to_constr typ in
        evd:=evd';
        rect_lemma,typ
 
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f96b189c5..ced572466 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -898,7 +898,7 @@ struct
 
   let has_typ gl t1 typ = 
    let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
-   Constr.equal ty typ
+   EConstr.eq_constr (Tacmach.project gl) ty (EConstr.of_constr typ)
 
 
   let is_convertible gl t1 t2 = 
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 131ecad33..c0eeff8d7 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -344,6 +344,8 @@ let _ = add_map "ring"
 (****************************************************************************)
 (* Ring database *)
 
+let pr_constr c = pr_constr (EConstr.Unsafe.to_constr c)
+
 module Cmap = Map.Make(Constr)
 
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
@@ -357,12 +359,12 @@ let find_ring_structure env sigma l =
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
-          if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
+          if not (Reductionops.is_conv env sigma ty ty') then
             user_err ~hdr:"ring"
               (str"arguments of ring_simplify do not have all the same type")
         in
         List.iter check cl';
-        (try ring_for_carrier ty
+        (try ring_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
           user_err ~hdr:"ring"
             (str"cannot find a declared ring structure over"++
@@ -495,7 +497,6 @@ let op_smorph r add mul req m1 m2 =
 (*         (setoid,op_morph) *)
 
 let ring_equality env evd (r,add,mul,opp,req) =
-  let pr_constr c = pr_constr (EConstr.to_constr !evd c) in
   match EConstr.kind !evd req with
     | App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
 	let setoid = plapp evd coq_eq_setoid [|r|] in
@@ -553,7 +554,6 @@ let build_setoid_params env evd r add mul opp req eqth =
 
 let dest_ring env sigma th_spec =
   let th_typ = Retyping.get_type_of env sigma th_spec in
-  let th_typ = EConstr.of_constr th_typ in
   match EConstr.kind sigma th_typ with
       App(f,[|r;zero;one;add;mul;sub;opp;req|])
         when eq_constr_nounivs sigma f (Lazy.force coq_almost_ring_theory) ->
@@ -585,7 +585,6 @@ let interp_cst_tac env sigma rk kind (zero,one,add,mul,opp) cst_tac =
 
 let make_hyp env evd c =
   let t = Retyping.get_type_of env !evd c in
-  let t = EConstr.of_constr t in
    plapp evd coq_mkhypo [|t;c|]
 
 let make_hyp_list env evd lH =
@@ -820,7 +819,6 @@ let sf_sr = my_reference"SF_SR"
 let dest_field env evd th_spec =
   let open Termops in
   let th_typ = Retyping.get_type_of env !evd th_spec in
-  let th_typ = EConstr.of_constr th_typ in
   match EConstr.kind !evd th_typ with
     | App(f,[|r;zero;one;add;mul;sub;opp;div;inv;req|])
         when is_global !evd (Lazy.force afield_theory) f ->
@@ -852,12 +850,12 @@ let find_field_structure env sigma l =
         let ty = Retyping.get_type_of env sigma t in
         let check c =
           let ty' = Retyping.get_type_of env sigma c in
-          if not (Reductionops.is_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr ty')) then
+          if not (Reductionops.is_conv env sigma ty ty') then
             user_err ~hdr:"field"
               (str"arguments of field_simplify do not have all the same type")
         in
         List.iter check cl';
-        (try field_for_carrier ty
+        (try field_for_carrier (EConstr.to_constr sigma ty)
         with Not_found ->
           user_err ~hdr:"field"
             (str"cannot find a declared field structure over"++
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index d34c9325e..9798fa11c 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1390,9 +1390,10 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
   let concl0 = pf_concl gl in
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
-  let gl, tty = pf_type_of gl (EConstr.of_constr t) in
-  let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
-  let concl = EConstr.of_constr concl in
+  let t = EConstr.of_constr t in
+  let concl_x = EConstr.of_constr concl_x in
+  let gl, tty = pf_type_of gl t in
+  let concl = EConstr.mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
 (* Register "ssrpattern" tactic *)