X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FcicNotationParser.ml;h=451d03a101de6273a20d566dc0e1103e06abb6e3;hb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;hp=53c60820c78632bd58f3b8527d697897537c92ff;hpb=fb9f80d2fb30216cc0754e8e8d09206f3e3e7bb7;p=helm.git

diff --git a/matitaB/components/content_pres/cicNotationParser.ml b/matitaB/components/content_pres/cicNotationParser.ml
index 53c60820c..451d03a10 100644
--- a/matitaB/components/content_pres/cicNotationParser.ml
+++ b/matitaB/components/content_pres/cicNotationParser.ml
@@ -338,7 +338,7 @@ let fold_exists terms ty body =
   List.fold_right
     (fun term body ->
       let lambda = Ast.Binder (`Lambda, (term, ty), body) in
-      Ast.Appl [ Ast.Symbol ("exists", 0); lambda ])
+      Ast.Appl [ Ast.Symbol ("exists", None); lambda ])
     terms body
 
 let fold_binder binder pt_names body =
@@ -589,12 +589,12 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
-    | id = PIDENT -> Ast.Ident (id, None), None
-    | SYMBOL "_" -> Ast.Ident ("_", None), None
+    | id = PIDENT -> Ast.Ident (id, `Ambiguous), None
+    | SYMBOL "_" -> Ast.Ident ("_", `Ambiguous), None
     | LPAREN; id = PIDENT; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident (id, None), Some typ
+        Ast.Ident (id, `Ambiguous), Some typ
     | LPAREN; SYMBOL "_"; SYMBOL ":"; typ = term; RPAREN ->
-        Ast.Ident ("_", None), Some typ
+        Ast.Ident ("_", `Ambiguous), Some typ
     ]
   ];
   match_pattern: [
@@ -615,24 +615,24 @@ EXTEND
   arg: [
     [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
       SYMBOL ":"; ty = term; RPAREN ->
-        List.map (fun n -> Ast.Ident (n, None)) names, Some ty
-    | name = IDENT -> [Ast.Ident (name, None)], None
+        List.map (fun n -> Ast.Ident (n, `Ambiguous)) names, Some ty
+    | name = IDENT -> [Ast.Ident (name, `Ambiguous)], None
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _) -> [meta], None
-        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", None)], None
+        | Ast.Variable (Ast.TermVar ("_",_)) -> [Ast.Ident ("_", `Ambiguous)], None
         | _ -> failwith "Invalid bound name."
    ]
   ];
   single_arg: [
-    [ name = IDENT -> Ast.Ident (name, None)
+    [ name = IDENT -> Ast.Ident (name, `Ambiguous)
     | blob = UNPARSED_META ->
         let meta = parse_level2_meta grammars (Ulexing.from_utf8_string blob) in
         match meta with
         | Ast.Variable (Ast.FreshVar _)
         | Ast.Variable (Ast.IdentVar _) -> meta
-        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", None)
+        | Ast.Variable (Ast.TermVar ("_",_)) -> Ast.Ident ("_", `Ambiguous)
         | _ -> failwith "Invalid index name."
     ]
   ];
@@ -692,7 +692,7 @@ EXTEND
     [ vars = [ l =
         [ l = LIST1 single_arg SEP SYMBOL "," -> l
         | l = LIST1 [ PIDENT | SYMBOL "_" ] SEP SYMBOL "," -> 
-            List.map (fun x -> Ast.Ident(x,None)) l
+            List.map (fun x -> Ast.Ident(x,`Ambiguous)) l
       ] -> l ];
       typ = OPT [ SYMBOL ":"; t = term -> t ] -> (vars, typ)
     ]
@@ -713,7 +713,7 @@ EXTEND
       [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
 	  id, Some typ
       | id = IDENT; ty = OPT [ SYMBOL ":"; typ = term -> typ] ->
-	  Ast.Ident(id,None), ty ];
+	  Ast.Ident(id,`Ambiguous), ty ];
       SYMBOL <:unicode<def>> (* ≝ *);
       p1 = term; "in"; p2 = term ->
         return_term loc (Ast.LetIn (var, p1, p2))
@@ -745,13 +745,15 @@ EXTEND
     ];
   term: LEVEL "90"
     [
-      [ id = IDENT -> return_term loc (Ast.Ident (id, None))
-      | id = IDENT; s = explicit_subst ->
-          return_term loc (Ast.Ident (id, Some s))
-      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, 0))
-      | u = URI -> return_term loc (Ast.Uri (u, None))
+      [ id = IDENT -> return_term loc (Ast.Ident (id, `Ambiguous))
+      | id = IDENT; s = explicit_subst -> (* XXX: no more explicit subst? *)
+          assert false
+          (* return_term loc (Ast.Ident (id, Some s))*)
+      | s = CSYMBOL -> return_term loc (Ast.Symbol (s, None))
+      | u = URI -> return_term loc (Ast.Ident 
+                     (NUri.name_of_uri (NUri.uri_of_string u), `Uri u))
       | r = NREF -> return_term loc (Ast.NRef (NReference.reference_of_string r))
-      | n = NUMBER -> return_term loc (Ast.Num (n, 0))
+      | n = NUMBER -> return_term loc (Ast.Num (n, None))
       | IMPLICIT -> return_term loc (Ast.Implicit `JustOne)
       | SYMBOL <:unicode<ldots>> -> return_term loc (Ast.Implicit `Vector)
       | PLACEHOLDER -> return_term loc Ast.UserInput