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, 3 insertions, 6 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"