fix double app in Ast

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index ae6284cc8a6eb01a2ee47bb172c3617a025e73bd..4bfeab669066ad762d7a260515c8a5426ab16a69 100644 (file)
--- 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)