From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 May 2008 19:03:13 +0000 (+0000)
Subject: revert last commit, context' -> context (added comment)
X-Git-Tag: make_still_working~5161
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d005e7130f74df3db81828c0fe7f3439a25d5002;hp=cc77c0daec24d9b0eeb054b630a9a5b9604c8f4d;p=helm.git

revert last commit, context' -> context (added comment)
---

diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml
index 237edff30..41c24c9ae 100644
--- a/helm/software/components/cic_disambiguation/disambiguate.ml
+++ b/helm/software/components/cic_disambiguation/disambiguate.ml
@@ -380,7 +380,9 @@ let interpretate_term ?(create_dummy_ids=false) ~(context: Cic.name list) ~env ~
                 if localize then
                  match body with
                     CicNotationPt.AttributedTerm (_,CicNotationPt.Appl(_::l)) ->
-                     let l' = List.map (aux ~localize loc context') l in
+                     (* since we avoid the letin, the context has no
+                      * recfuns in it *)
+                     let l' = List.map (aux ~localize loc context) l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
                 else