From cf78c7adc2f4933e055df9ea4954eee455a70d74 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Oct 2002 06:08:09 +0000
Subject: Prise en compte let-in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3187 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/library/impargs.ml b/library/impargs.ml
index cc9d3f8cae..2719374185 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -92,7 +92,7 @@ let is_flexible_reference env bound depth f =
   match kind_of_term f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
-    | Rel n -> (* internal variable [TODO: deal local definitions] *) false
+    | Rel n -> (* since local definitions have been expanded *) false
     | Const kn ->
         let cb = Environ.lookup_constant kn env in
         cb.const_body <> None & not cb.const_opaque
@@ -110,6 +110,8 @@ let add_free_rels_until bound env m pos acc =
         iter_constr_with_binders succ (frec false) depth c
     | Case _ ->
         iter_constr_with_binders succ (frec false) depth c
+    | LetIn (_,b,_,c) ->
+        frec rig depth (subst1 b c)
     | _ ->
         iter_constr_with_binders succ (frec rig) depth c
   in 
@@ -470,4 +472,3 @@ let _ =
 let rollback f x =
   let fs = freeze () in
   try f x with e -> begin unfreeze fs; raise e end
-
-- 
cgit v1.2.3