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 237edff305dc52821b64b303d469140c95bf7124..41c24c9ae5a11065df8c8ccc9e5c632911c60cac 100644 (file)
--- 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