From f42d23df32484582ebba6fdafd23e873c0acf90d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 19 Apr 2011 08:06:07 +0000 Subject: [PATCH] disambiguation of explicit interprettions with arguments now works i.e. 'eq x y z --- matita/components/ng_disambiguation/nCicDisambiguate.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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) -- 2.39.2