Inv API using EConstr.

5 files changed, 16 insertions, 9 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ff3424c44..cdaa4e9ee 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -99,6 +99,8 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
   let build_one_branch i cty =
     let typi = type_constructor mind mib u cty params in
     let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
+    let decl = List.map (on_snd EConstr.Unsafe.to_constr) decl in
+    let indapp = EConstr.Unsafe.to_constr indapp in
     let decl_with_letin,_ = decompose_prod_assum typi in
     let ind,cargs = find_rectype_a env indapp in
     let nparams = Array.length params in
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index f09f3221d..3230f92da 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -203,7 +203,8 @@ let compute_canonical_projections warn (con,ind) =
   let ctx = Univ.ContextSet.of_context ctx in
   let c = Environ.constant_value_in env (con,u) in
   let lt,t = Reductionops.splay_lam env Evd.empty (EConstr.of_constr c) in
-  let lt = List.rev_map snd lt in
+  let t = EConstr.Unsafe.to_constr t in
+  let lt = List.rev_map (snd %> EConstr.Unsafe.to_constr) lt in
   let args = snd (decompose_app t) in
   let { s_EXPECTEDPARAM = p; s_PROJ = lpj; s_PROJKIND = kl } =
     lookup_structure ind in
@@ -303,6 +304,7 @@ let check_and_decompose_canonical_structure ref =
     | Some vc -> vc
     | None -> error_not_structure ref in
   let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in
+  let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind_of_term body with
     | App (f,args) -> f,args
     | _ -> error_not_structure ref in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 0dd615bfb..480ec2319 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1453,13 +1453,13 @@ let hnf_lam_applist env sigma t nl =
   List.fold_left (fun acc t -> hnf_lam_app env sigma (EConstr.of_constr acc) t) (EConstr.Unsafe.to_constr t) nl
 
 let bind_assum (na, t) =
-  let inj = EConstr.Unsafe.to_constr in
-  (na, inj t)
+  (na, t)
 
 let splay_prod env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1470,7 +1470,8 @@ let splay_prod env sigma =
 let splay_lam env sigma =
   let rec decrec env m c =
     let t = whd_all env sigma c in
-    match EConstr.kind sigma (EConstr.of_constr t) with
+    let t = EConstr.of_constr t in
+    match EConstr.kind sigma t with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (local_assum (n,a)) env)
 	    (bind_assum (n,a)::m) c0
@@ -1498,7 +1499,7 @@ let splay_prod_assum env sigma =
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
-  match EConstr.kind sigma (EConstr.of_constr c) with
+  match EConstr.kind sigma c with
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 864b1a625..e67fad3fd 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -213,9 +213,9 @@ val hnf_lam_app      : env ->  evar_map -> EConstr.t -> EConstr.t -> constr
 val hnf_lam_appvect  : env ->  evar_map -> EConstr.t -> EConstr.t array -> constr
 val hnf_lam_applist  : env ->  evar_map -> EConstr.t -> EConstr.t list -> constr
 
-val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * constr
-val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * constr
-val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * constr) list * sorts
+val splay_prod : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
+val splay_lam : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * EConstr.constr
+val splay_arity : env ->  evar_map -> EConstr.t -> (Name.t * EConstr.constr) list * sorts
 val sort_of_arity : env -> evar_map -> EConstr.t -> sorts
 val splay_prod_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
 val splay_lam_n : env ->  evar_map -> int -> EConstr.t -> Context.Rel.t * constr
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 60f99fd3d..31693d82f 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -106,6 +106,8 @@ let build_branches_type env sigma (mind,_ as _ind) mib mip u params dep p =
   let build_one_branch i cty =
     let typi = type_constructor mind mib u cty params in
     let decl,indapp = Reductionops.splay_prod env sigma (EConstr.of_constr typi) in
+    let decl = List.map (on_snd EConstr.Unsafe.to_constr) decl in
+    let indapp = EConstr.Unsafe.to_constr indapp in
     let decl_with_letin,_ = decompose_prod_assum typi in
     let ((ind,u),cargs) = find_rectype_a env indapp in
     let nparams = Array.length params in