diff options
| author | herbelin | 2002-10-29 06:08:09 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-29 06:08:09 +0000 |
| commit | cf78c7adc2f4933e055df9ea4954eee455a70d74 (patch) | |
| tree | b270673e3cc9313da6b3883d9ad8a898ce451171 | |
| parent | a7347a87051c8cbb11d4777667223db4a4164534 (diff) | |
Prise en compte let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3187 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/impargs.ml | 5 |
1 files 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 - |