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

1 files changed, 4 insertions, 9 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index fcae3341e..b0387417c 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