Removing compatibility layers in Retyping

6 files changed, 13 insertions, 12 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index a428ab0ed..393e958d3 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -62,7 +62,7 @@ let refresh_undefined_univs clenv =
 
 let clenv_hnf_constr ce t = hnf_constr (cl_env ce) (cl_sigma ce) t
 
-let clenv_get_type_of ce c = EConstr.of_constr (Retyping.get_type_of (cl_env ce) (cl_sigma ce) c)
+let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 
 exception NotExtensibleClause
 
@@ -673,9 +673,7 @@ let evar_of_binder holes = function
 let define_with_type sigma env ev c =
   let open EConstr in
   let t = Retyping.get_type_of env sigma ev in
-  let t = EConstr.of_constr t in
   let ty = Retyping.get_type_of env sigma c in
-  let ty = EConstr.of_constr ty in
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true (Loc.ghost) env sigma j t in
   let (ev, _) = destEvar sigma ev in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 98ad9ebe3..8b890f6f8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -331,7 +331,7 @@ let meta_free_prefix sigma a =
 
 let goal_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)
+  else EConstr.Unsafe.to_constr (Retyping.get_type_of env sigma (EConstr.of_constr c))
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = Goal.V82.env sigma goal in
@@ -341,6 +341,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   in
     if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
       let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
+      let t'ty = EConstr.Unsafe.to_constr t'ty in
       let sigma = check_conv_leq_goal env sigma trm t'ty conclty in
         (goalacc,t'ty,sigma,trm)
     else
@@ -377,6 +378,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	      let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in
 	        type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args)
 	    in
+	    let ty = EConstr.Unsafe.to_constr ty in
 	      goalacc, ty, sigma, f
 	  else
 	    mk_hdgoals sigma goal goalacc f
@@ -390,6 +392,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	let c = mkProj (p, c') in
 	let ty = get_type_of env sigma (EConstr.of_constr c) in
+	let ty = EConstr.Unsafe.to_constr ty in
 	  (acc',ty,sigma,c)
 
       | Case (ci,p,c,lf) ->
@@ -439,7 +442,7 @@ and mk_hdgoals sigma goal goalacc trm =
 	  if is_template_polymorphic env sigma (EConstr.of_constr f)
 	  then
 	    let l' = meta_free_prefix sigma l in
-	   (goalacc,type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l',sigma,f)
+	   (goalacc,EConstr.Unsafe.to_constr (type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) l'),sigma,f)
 	  else mk_hdgoals sigma goal goalacc f
 	in
 	let ((acc'',conclty',sigma), args) = mk_arggoals sigma goal acc' hdty l in
@@ -465,6 +468,7 @@ and mk_hdgoals sigma goal goalacc trm =
          let (acc',cty,sigma,c') = mk_hdgoals sigma goal goalacc c in
 	 let c = mkProj (p, c') in
          let ty = get_type_of env sigma (EConstr.of_constr c) in
+         let ty = EConstr.Unsafe.to_constr ty in
 	   (acc',ty,sigma,c)
 
     | _ ->
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index a830e25d9..8878051c8 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -25,7 +25,7 @@ open Misctypes
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env sigma c =
   let ctyp = Retyping.get_type_of env sigma c in
-  Vnorm.cbv_vm env sigma c (EConstr.of_constr ctyp)
+  Vnorm.cbv_vm env sigma c ctyp
 
 let warn_native_compute_disabled =
   CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
@@ -38,7 +38,7 @@ let cbv_native env sigma c =
      cbv_vm env sigma c)
   else
     let ctyp = Retyping.get_type_of env sigma c in
-    Nativenorm.native_norm env sigma c (EConstr.of_constr ctyp)
+    Nativenorm.native_norm env sigma c ctyp
 
 let whd_cbn flags env sigma t =
   let (state,_) =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 32064aff5..c36bb143e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -135,7 +135,6 @@ let refine ?(unsafe = true) f =
 
 let with_type env evd c t =
   let my_type = Retyping.get_type_of env evd c in
-  let my_type = EConstr.of_constr my_type in
   let j = Environ.make_judge c my_type in
   let (evd,j') =
     Coercion.inh_conv_coerce_to true (Loc.ghost) env evd j t
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index d9caadd54..7ffb30fa8 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -108,7 +108,7 @@ let pf_const_value              = pf_reduce (fun env _ -> constant_value_in env)
 let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind
 let pf_reduce_to_atomic_ind     = pf_reduce reduce_to_atomic_ind
 
-let pf_hnf_type_of gls          = pf_get_type_of gls %> EConstr.of_constr %> pf_whd_all gls
+let pf_hnf_type_of gls          = pf_get_type_of gls %> pf_whd_all gls
 
 let pf_is_matching gl p c       = pf_apply Constr_matching.is_matching_conv gl p c
 let pf_matches gl p c           = pf_apply Constr_matching.matches_conv gl p c
@@ -234,7 +234,7 @@ module New = struct
 
   let pf_hnf_constr gl t = pf_apply hnf_constr gl t
   let pf_hnf_type_of gl t =
-    pf_whd_all gl (EConstr.of_constr (pf_get_type_of gl t))
+    pf_whd_all gl (pf_get_type_of gl t)
 
   let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t
 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 06b3e3981..f0471bf66 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -41,7 +41,7 @@ val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> EConstr.constr -> types
-val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * types
+val pf_type_of            : goal sigma -> EConstr.constr -> evar_map * EConstr.types
 val pf_hnf_type_of        : goal sigma -> EConstr.constr -> EConstr.types
 
 val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
@@ -109,7 +109,7 @@ module New : sig
   val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> EConstr.types
 
   val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> Term.types
-  val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * Term.types
+  val pf_type_of : ('a, 'r) Proofview.Goal.t -> EConstr.constr -> evar_map * EConstr.types
   val pf_conv_x : ('a, 'r) Proofview.Goal.t -> EConstr.t -> EConstr.t -> bool
 
   val pf_get_new_id  : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier