From f57b2e6cf26316ec7df340ab95399039dae5143e Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 18 Jan 2008 17:20:28 +0000
Subject: bug in accessing n-th abstraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10451 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/sign.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/sign.ml b/kernel/sign.ml
index 79619b48f1..218ac6c483 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -181,7 +181,9 @@ let decompose_prod_n_assum n =
   prodec_rec empty_rel_context n
 
 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T 
-   into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+   into the pair ([(xn,Tn);...;(x1,T1)],T)
+   Lets in between are not expanded but turn into local definitions,
+   but n is the actual number of destructurated lambdas.  *)
 let decompose_lam_n_assum n =
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
@@ -189,7 +191,7 @@ let decompose_lam_n_assum n =
     if n=0 then l,c 
     else match kind_of_term c with 
     | Lambda (x,t,c)  -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c
-    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c
+    | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) n c
     | Cast (c,_,_)      -> lamdec_rec l n c
     | c -> error "decompose_lam_n_assum: not enough abstractions"
   in 
-- 
cgit v1.2.3