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

18 files changed, 35 insertions, 64 deletions

diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index e7610923cd..b99a3621d8 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -138,7 +138,7 @@ let (loop_ids : tactic) = fun gl ->
 	  then
 	    tclTHEN (clear [id]) (arec al) gl
 	  else if n >= 7 & String.sub s 0 7 = "Variant" then begin
-	    match pf_matches gl eq_pattern (body_of_type a) with
+	    match pf_matches gl eq_pattern a with
 	      | [_; _,varphi; _] when isVar varphi ->
 		  let phi = destVar varphi in
 		  if Termops.occur_var env phi concl then
@@ -159,7 +159,6 @@ let (assumption_bis : tactic) = fun gl ->
   let rec arec = function
     | [] -> Util.error "No such assumption"
     | (s,a) :: al ->
-	let a = body_of_type a in
 	if pf_conv_x_leq gl a concl then 
           refine (mkVar s) gl
 	else if pf_is_matching gl and_pattern a then
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 16705262d3..d97e649701 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -492,7 +492,7 @@ let rec fourier gl=
       in tac gl)
      with _ -> 
     (* les hypothèses *)
-    let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
+    let hyps = List.map (fun (h,t)-> (mkVar h,t))
                         (list_of_sign (pf_hyps gl)) in
     let lineq =ref [] in
     List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index bbde91aac3..b0a34cfd12 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -135,13 +135,13 @@ let implicits_to_ast_list implicits =
 let make_variable_ast name typ implicits =
   (VernacAssumption
     ((Local,Definitional),false,(*inline flag*)
-     [false,([dummy_loc,name], constr_to_ast (body_of_type typ))]))
+     [false,([dummy_loc,name], constr_to_ast typ)]))
   ::(implicits_to_ast_list implicits);;
     
 
 let make_definition_ast name c typ implicits =
   VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None,
-    (constr_to_ast c), Some (constr_to_ast (body_of_type typ))),
+    (constr_to_ast c), Some (constr_to_ast typ)),
     (fun _ _ -> ()))
   ::(implicits_to_ast_list implicits);;
 
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index 27efe04702..c1889b689c 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -1772,8 +1772,7 @@ let subst_rel_context k ctx subst =
 let lift_rel_contextn n k sign =
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k-1) sign)
+	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
   liftrec (rel_context_length sign + k) sign
@@ -2066,8 +2065,7 @@ let build_dependent_signature env evars avoid tomatchs arsign =
 let liftn_rel_context n k sign =  
   let rec liftrec k = function
     | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k-1) sign)
+	(na,option_map (liftn n k) c,liftn n k t)::(liftrec (k-1) sign)
     | [] -> []
   in
     liftrec (k + rel_context_length sign) sign
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index c2132f61b5..ab542feb20 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -67,8 +67,6 @@ module SubtacPretyping_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 *)
@@ -113,7 +111,7 @@ module SubtacPretyping_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/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml
index 8a5967a23c..75e428e14d 100644
--- a/contrib/xml/cic2acic.ml
+++ b/contrib/xml/cic2acic.ml
@@ -241,16 +241,15 @@ let typeur sigma metamap =
     | T.Var id ->
         (try
           let (_,_,ty) = Environ.lookup_named id env in
-          T.body_of_type ty
+          ty
         with Not_found ->
           Util.anomaly ("type_of: variable "^(Names.string_of_id id)^" unbound"))
     | T.Const c ->
         let cb = Environ.lookup_constant c env in
         Typeops.type_of_constant_type env (cb.Declarations.const_type)
     | T.Evar ev -> Evd.existential_type sigma ev
-    | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind)
-    | T.Construct cstr ->
-       T.body_of_type (Inductiveops.type_of_constructor env cstr)
+    | T.Ind ind -> Inductiveops.type_of_inductive env ind
+    | T.Construct cstr -> Inductiveops.type_of_constructor env cstr
     | T.Case (_,p,c,lf) ->
         let Inductiveops.IndType(_,realargs) =
           try Inductiveops.find_rectype env sigma (type_of env c)
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index cce788912d..de8c540caf 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -51,7 +51,7 @@ let type_judgment env sigma j =
 ;;
 
 let type_judgment_cprop env sigma j =
-  match Term.kind_of_term(whd_betadeltaiotacprop env sigma (Term.body_of_type j.Environ.uj_type)) with
+  match Term.kind_of_term(whd_betadeltaiotacprop env sigma j.Environ.uj_type) with
     | Term.Sort s -> Some {Environ.utj_val = j.Environ.uj_val; Environ.utj_type = s }
     | _ -> None  (* None means the CProp constant *)
 ;;
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 0127132399..1aabd4348e 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -329,14 +329,13 @@ let mk_variable_obj id body typ =
   let variables = search_variables () in
   let params = filter_params variables hyps'' in
    Acic.Variable
-    (Names.string_of_id id, unsharedbody,
-     (Unshare.unshare (Term.body_of_type typ)), params)
+    (Names.string_of_id id, unsharedbody, Unshare.unshare typ, params)
 ;;
 
 (* Unsharing is not performed on the body, that must be already unshared. *)
 (* The evar map and the type, instead, are unshared by this function.     *)
 let mk_current_proof_obj is_a_variable id bo ty evar_map env =
- let unshared_ty = Unshare.unshare (Term.body_of_type ty) in
+ let unshared_ty = Unshare.unshare ty in
  let metasenv =
   List.map
    (function
@@ -384,7 +383,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env =
 
 let mk_constant_obj id bo ty variables hyps =
  let hyps = string_list_of_named_context_list hyps in
- let ty = Unshare.unshare (Term.body_of_type ty) in
+ let ty = Unshare.unshare ty in
  let params = filter_params variables hyps in
   match bo with
      None ->
@@ -413,7 +412,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
         let cons =
          (Array.fold_right (fun (name,lc) i -> (name,lc)::i)
           (Array.mapi
-           (fun j x ->(x,Unshare.unshare (Term.body_of_type lc.(j)))) consnames)
+           (fun j x ->(x,Unshare.unshare lc.(j))) consnames)
           []
          )
         in
diff --git a/kernel/environ.ml b/kernel/environ.ml
index e69f63d24d..4266602983 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -58,9 +58,7 @@ let push_rel = push_rel
 let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x
     
 let push_rec_types (lna,typarray,_) env =
-  let ctxt =
-    array_map2_i
-      (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in
+  let ctxt = array_map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> push_rel assum e) env ctxt
     
 let reset_rel_context env =
diff --git a/kernel/sign.ml b/kernel/sign.ml
index f5d6c3b29f..c2b4eca750 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -92,7 +92,7 @@ let push_named_to_rel_context hyps ctxt =
   let rec push = function
     | (id,b,t) :: l ->
 	let s, hyps = push l in
-	let d = (Name id, option_map (subst_vars s) b, type_app (subst_vars s) t) in
+	let d = (Name id, option_map (subst_vars s) b, subst_vars s t) in
 	id::s, d::hyps
     | [] -> [],[] in
   let s, hyps = push hyps in
diff --git a/kernel/term.ml b/kernel/term.ml
index 5f9a3ff93d..4b01ac1cfe 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -636,10 +636,6 @@ type types = constr
 
 type strategy = types option 
 
-let type_app f tt = f tt
-
-let body_of_type ty = ty
-
 type named_declaration = identifier * constr option * types
 type rel_declaration = name * constr option * types
 
diff --git a/kernel/term.mli b/kernel/term.mli
index fcae3341e4..b0387417cc 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -61,18 +61,13 @@ type constr
    and application grouping *)
 val eq_constr : constr -> constr -> bool
 
-(* [types] is the same as [constr] but is intended to be used where a
-   {\em type} in CCI sense is expected (Rem:plurial form since [type] is a
-   reserved ML keyword) *)
+(* [types] is the same as [constr] but is intended to be used for
+   documentation to indicate that such or such function specifically works
+   with {\em types} (i.e. terms of type a sort). 
+   (Rem:plurial form since [type] is a reserved ML keyword) *)
 
 type types = constr
 
-(*s Functions about [types] *)
-
-val type_app : (constr -> constr) -> types -> types
-
-val body_of_type : types -> constr
-
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 9b8735fa72..a09b0799b8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -82,7 +82,7 @@ let judge_of_relative env n =
   try
     let (_,_,typ) = lookup_rel n env in
     { uj_val  = mkRel n;
-      uj_type = type_app (lift n) typ }
+      uj_type = lift n typ }
   with Not_found -> 
     error_unbound_rel env n
 
@@ -192,7 +192,7 @@ let judge_of_abstraction env name var j =
 
 let judge_of_letin env name defj typj j =
   { uj_val = mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val) ;
-    uj_type = type_app (subst1 defj.uj_val) j.uj_type }
+    uj_type = subst1 defj.uj_val j.uj_type }
 
 (* Type of an application. *)
 
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