From d005e7130f74df3db81828c0fe7f3439a25d5002 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sun, 18 May 2008 19:03:13 +0000
Subject: [PATCH] revert last commit, context' -> context (added comment)

---
 helm/software/components/cic_disambiguation/disambiguate.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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
-- 
2.39.2