Suppression des type_app et body_of_type qui alourdissent inutilement le code

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10098 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 12 insertions, 23 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 4a0f12d66c..26ccc8024b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -51,7 +51,7 @@ let j_nf_evar sigma j =
 let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
 let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
-  {utj_val=type_app (nf_evar sigma) v;utj_type=t}
+  {utj_val=nf_evar sigma v;utj_type=t}
 
 let env_ise sigma env =
   let sign = named_context_val env in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index c5742268b1..add975cf38 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -193,8 +193,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	
   let mt_evd = Evd.empty
     
-  let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
-      
   (* Utilisé pour inférer le prédicat des Cases *)
   (* Semble exagérement fort *)
   (* Faudra préférer une unification entre les types de toutes les clauses *)
@@ -246,7 +244,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
     let id = strip_meta id in (* May happen in tactics defined by Grammar *)
       try
 	let (n,typ) = lookup_rel_id id (rel_context env) in
-	  { uj_val  = mkRel n; uj_type = type_app (lift n) typ }
+	  { uj_val  = mkRel n; uj_type = lift n typ }
       with Not_found ->
 	try
 	  List.assoc id lvar
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d01c5679cc..f15ec51669 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -214,7 +214,7 @@ let push_named_rec_types (lna,typarray,_) env =
     array_map2_i
       (fun i na t ->
 	 match na with
-	   | Name id -> (id, None, type_app (lift i) t)
+	   | Name id -> (id, None, lift i t)
 	   | Anonymous -> anomaly "Fix declarations must be named")
       lna typarray in
   Array.fold_left
@@ -305,11 +305,8 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    (co-)fixpoint) *)
 
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt =
-    array_map2_i
-      (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in
-  Array.fold_left
-    (fun e assum -> g assum e) e ctxt
+  let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  Array.fold_left (fun e assum -> g assum e) e ctxt
 
 
 let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
@@ -670,7 +667,7 @@ let subst_term_occ_decl locs c (id,bodyopt,typ as d) =
     | None -> (id,None,subst_term_occ locs c typ)
     | Some body -> 
 	if locs = [] then
-	  (id,Some (subst_term c body),type_app (subst_term c) typ)
+	  (id,Some (subst_term c body),subst_term c typ)
 	else if List.mem 0 locs then 
 	  d
 	else 
@@ -753,20 +750,18 @@ let named_hd env a = function
   | Anonymous -> Name (id_of_string (hdchar env a)) 
   | x         -> x
 
-let named_hd_type env a = named_hd env (body_of_type a)
-
-let mkProd_name   env (n,a,b) = mkProd (named_hd_type env a n, a, b)
-let mkLambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b)
+let mkProd_name   env (n,a,b) = mkProd (named_hd env a n, a, b)
+let mkLambda_name env (n,a,b) = mkLambda (named_hd env a n, a, b)
 
 let lambda_name = mkLambda_name
 let prod_name = mkProd_name
 
-let prod_create   env (a,b) = mkProd (named_hd_type env a Anonymous, a, b)
-let lambda_create env (a,b) =  mkLambda (named_hd_type env a Anonymous, a, b)
+let prod_create   env (a,b) = mkProd (named_hd env a Anonymous, a, b)
+let lambda_create env (a,b) =  mkLambda (named_hd env a Anonymous, a, b)
 
 let name_assumption env (na,c,t) =
   match c with
-    | None      -> (named_hd_type env t na, None, t)
+    | None      -> (named_hd env t na, None, t)
     | Some body -> (named_hd env body na, c, t)
 
 let name_context env hyps =
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 17207cf577..f215d4e9ae 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -157,7 +157,6 @@ val hdchar : env -> types -> string
 val id_of_name_using_hdchar :
   env -> types -> name -> identifier
 val named_hd : env -> types -> name -> name
-val named_hd_type : env -> types -> name -> name
 
 val mkProd_name : env -> name * types * types -> types
 val mkLambda_name : env -> name * types * constr -> constr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5497d98d18..346942f1e8 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -26,9 +26,6 @@ let meta_type evd mv =
     with Not_found -> error ("unknown meta ?"^string_of_int mv) in
   meta_instance evd ty
 
-let vect_lift = Array.mapi lift
-let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t)
-
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> j.uj_type) jl in
   type_of_constant_knowing_parameters env (constant_type env cst) paramstyp
@@ -170,7 +167,7 @@ let mcheck env evd c t =
 let mtype_of env evd c =
   let j = execute env evd (nf_evar (evars_of evd) c) in
   (* No normalization: it breaks Pattern! *)
-  (*nf_betaiota*) (body_of_type j.uj_type)
+  (*nf_betaiota*) j.uj_type
 
 let msort_of env evd c =
   let j = execute env evd (nf_evar (evars_of evd) c) in