From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 28 Nov 2008 16:18:11 +0000 (+0000)
Subject: \forall x:?. and \forall x. both generate a meta for a type
X-Git-Tag: make_still_working~4480
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=aa941d8c9c451264a721364db1e412b877d4a08f;p=helm.git

\forall x:?. and \forall x. both generate a meta for a type
---

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