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

2 files changed, 7 insertions, 15 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 5c045a8ab0..a450e61b73 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -910,10 +910,6 @@ let lift k = liftn k 1
 
 let pop t = lift (-1) t
 
-let lift_context n l = 
-  let k = List.length l in 
-  list_map_i (fun i (name,c) -> (name,liftn n (k-i) c)) 0 l
-
 (*********************)
 (*   Substituting    *)
 (*********************)
@@ -1242,14 +1238,15 @@ let prod_applist t nL = List.fold_left prod_app t nL
 (* Other term destructors        *)
 (*********************************)
 
-type flat_arity = (name * constr) list * sorts
+type arity = rel_declaration list * sorts
 
 (* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
    ([(xn,Tn);...;(x1,T1)],T), where T is not a product *)
 let destArity = 
   let rec prodec_rec l c =
     match kind_of_term c with
-    | IsProd (x,t,c) -> prodec_rec ((x,t)::l) c
+    | IsProd (x,t,c) -> prodec_rec ((x,None,t)::l) c
+    | IsLetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c
     | IsCast (c,_)   -> prodec_rec l c
     | IsSort s       -> l,s
     | _              -> anomaly "decompose_arity: not an arity"
diff --git a/kernel/term.mli b/kernel/term.mli
index 7bba6d924e..66ba16db62 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