Ajout let dans destArity, suppression de lift_context (lift_rel_context suffit)

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

1 files changed, 4 insertions, 9 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 7bba6d924..66ba16db6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -62,8 +62,6 @@ type constr
 
 type typed_type
 
-type flat_arity = (name * constr) list * sorts
-
 (*s Functions about [typed_type] *)
 
 val make_typed : constr -> sorts -> typed_type
@@ -83,6 +81,8 @@ val outcast_type : constr -> typed_type
 type var_declaration = identifier * constr option * typed_type
 type rel_declaration = name * constr option * typed_type
 
+type arity = rel_declaration list * sorts
+
 (**********************************************************************)
 type global_reference =
   | ConstRef of section_path
@@ -256,7 +256,7 @@ val mkCoFix : cofixpoint -> constr
    raise [invalid_arg "dest*"] if the term has not the expected form. *)
 
 (* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *)
-val destArity : constr -> flat_arity
+val destArity : constr -> arity
 val isArity : constr -> bool
 
 (* Destructs a DeBrujin index *)
@@ -466,12 +466,7 @@ val lift : int -> constr -> constr
 (* [pop c] lifts by -1 the positive indexes in [c] *)
 val pop : constr -> constr
 
-(* [lift_context n ctxt] lifts terms in [ctxt] by [n] preserving
-   (i.e. not lifting) the internal references between terms of [ctxt];
-   more recent terms come first in [ctxt] *)
-val lift_context : int -> (name * constr) list -> (name * constr) list
-
-(* [substnl [a1;...;an] k c] substitutes in parallele [a1],...,[an]
+(* [substnl [a1;...;an] k c] substitutes in parallel [a1],...,[an]
     for respectively [Rel(k+1)],...,[Rel(k+n)] in [c]; it relocates
     accordingly indexes in [a1],...,[an] *)
 val substnl : constr list -> int -> constr -> constr