X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=4bfeab669066ad762d7a260515c8a5426ab16a69;hb=8f785ed7fd5b2674d9fadbe5fac2eb7b2ec1cc4b;hp=ae6284cc8a6eb01a2ee47bb172c3617a025e73bd;hpb=72a3999ca5a4a2168753c272063ea6530dc963bd;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index ae6284cc8..4bfeab669 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -19,8 +19,8 @@ open UriManager
 module Ast = CicNotationPt
 module NRef = NReference 
 
+let debug_print s = prerr_endline (Lazy.force s);;
 let debug_print _ = ();;
-(* let debug_print s = prerr_endline (Lazy.force s);; *)
 
 let cic_name_of_name = function
   | Ast.Ident (n, None) ->  n
@@ -119,6 +119,12 @@ let interpretate_term_and_interpretate_term_option
          NCicUntrusted.NCicHash.add localization_tbl res loc;
        res
     | CicNotationPt.AttributedTerm (_, term) -> aux ~localize loc context term
+    | CicNotationPt.Appl (CicNotationPt.Appl inner :: args) ->
+        aux ~localize loc context (CicNotationPt.Appl (inner @ args))
+    | CicNotationPt.Appl 
+        (CicNotationPt.AttributedTerm (att,(CicNotationPt.Appl inner))::args)->
+        aux ~localize loc context 
+          (CicNotationPt.AttributedTerm (att,CicNotationPt.Appl (inner @ args)))
     | CicNotationPt.Appl (CicNotationPt.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)