From aa941d8c9c451264a721364db1e412b877d4a08f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 28 Nov 2008 16:18:11 +0000 Subject: [PATCH 1/1] \forall x:?. and \forall x. both generate a meta for a type --- .../components/ng_disambiguation/nCicDisambiguate.ml | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml index 8c0874056..8dd4bc634 100644 --- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml +++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml @@ -20,6 +20,7 @@ module Ast = CicNotationPt module NRef = NReference let debug_print _ = ();; +(* let debug_print s = prerr_endline (Lazy.force s);; *) let cic_name_of_name = function | Ast.Ident (n, None) -> n @@ -376,6 +377,13 @@ patterns not implemented *) | _ -> assert false (* god bless Bologna *) and aux_option ~localize loc context annotation = function | None -> NCic.Implicit annotation + | Some (CicNotationPt.AttributedTerm (`Loc loc, term)) -> + let res = aux_option ~localize loc context annotation (Some term) in + if localize then NCicUntrusted.NCicHash.add localization_tbl res loc; + res + | Some (CicNotationPt.AttributedTerm (_, term)) -> + aux_option ~localize loc context annotation (Some term) + | Some CicNotationPt.Implicit -> NCic.Implicit annotation | Some term -> aux ~localize loc context term in aux ~localize:true HExtlib.dummy_floc context ast -- 2.39.2