\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 8c087405615bbe9360e4612944397688d5d967ab..8dd4bc634a60f74b85b24ae50fcbb6d2d711a45e 100644 (file)
--- 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