]> matita.cs.unibo.it Git - helm.git/commitdiff
a missing prime
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 9 May 2008 12:05:57 +0000 (12:05 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 9 May 2008 12:05:57 +0000 (12:05 +0000)
helm/software/components/cic_disambiguation/disambiguate.ml

index 4b17bef5dfa95eac5c2aabf11f643196c09f9d07..237edff305dc52821b64b303d469140c95bf7124 100644 (file)
@@ -380,7 +380,7 @@ 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
+                     let l' = List.map (aux ~localize loc context') l in
                       `AvoidLetIn (n,l')
                   | _ -> assert false
                 else