From: Ferruccio Guidi Date: Tue, 19 Apr 2011 08:06:07 +0000 (+0000) Subject: disambiguation of explicit interprettions with arguments now works X-Git-Tag: make_still_working~2533 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f42d23df32484582ebba6fdafd23e873c0acf90d;p=helm.git disambiguation of explicit interprettions with arguments now works i.e. 'eq x y z --- diff --git a/matita/components/ng_disambiguation/nCicDisambiguate.ml b/matita/components/ng_disambiguation/nCicDisambiguate.ml index 5c2de5caa..8c58b33c2 100644 --- a/matita/components/ng_disambiguation/nCicDisambiguate.ml +++ b/matita/components/ng_disambiguation/nCicDisambiguate.ml @@ -117,12 +117,12 @@ let interpretate_term_and_interpretate_term_option (status: #NCic.status) NCicUntrusted.NCicHash.add localization_tbl res loc; res | NotationPt.AttributedTerm (_, term) -> aux ~localize loc context term - | NotationPt.Appl (NotationPt.Appl inner :: args) -> - aux ~localize loc context (NotationPt.Appl (inner @ args)) | NotationPt.Appl - (NotationPt.AttributedTerm (att,(NotationPt.Appl inner))::args)-> + (NotationPt.AttributedTerm (att, inner)::args)-> aux ~localize loc context - (NotationPt.AttributedTerm (att,NotationPt.Appl (inner @ args))) + (NotationPt.AttributedTerm (att,NotationPt.Appl (inner :: args))) + | NotationPt.Appl (NotationPt.Appl inner :: args) -> + aux ~localize loc context (NotationPt.Appl (inner @ args)) | NotationPt.Appl (NotationPt.Symbol (symb, i) :: args) -> let cic_args = List.map (aux ~localize loc context) args in Disambiguate.resolve ~mk_choice ~env (Symbol (symb, i)) (`Args cic_args)