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 5c2de5caa90ba4e22758637b4feb54478d22ae35..8c58b33c2e4410191b1885edfc2c5448dc5a1000 100644 (file)
--- 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)