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, 8 insertions, 19 deletions

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. *)