X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2Fdisambiguate.ml;h=237edff305dc52821b64b303d469140c95bf7124;hb=df28d2c8f26ad18cc8b61b73adb1dfd8be31ec35;hp=4b17bef5dfa95eac5c2aabf11f643196c09f9d07;hpb=8568952f9d2f97524d1a150743fc91ca9d0c0d05;p=helm.git diff --git a/helm/software/components/cic_disambiguation/disambiguate.ml b/helm/software/components/cic_disambiguation/disambiguate.ml index 4b17bef5d..237edff30 100644 --- a/helm/software/components/cic_disambiguation/disambiguate.ml +++ b/helm/software/components/cic_disambiguation/disambiguate.ml @@ -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