From 8f785ed7fd5b2674d9fadbe5fac2eb7b2ec1cc4b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 1 Sep 2009 17:12:41 +0000 Subject: [PATCH] fix double app in Ast --- .../components/ng_disambiguation/nCicDisambiguate.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) 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) -- 2.39.2