X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=7473838ca5e6b6424e36017dc08b1c28cebe7c09;hb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;hp=6846c30b5b9e608fe96af08fbb60b740ccf24b19;hpb=fb9f80d2fb30216cc0754e8e8d09206f3e3e7bb7;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 6846c30b5..7473838ca 100644
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -75,7 +75,8 @@ let number s =
     (Ast.Literal (`Number s))
 
 let ident i =
-  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) (Ast.Ident (i, None))
+  add_xml_attrs (RenderingAttrs.ident_attributes `MathML) 
+    (Ast.Ident (i,`Ambiguous))
 
 let ident_w_href href i =
   match href with
@@ -89,7 +90,7 @@ let binder_symbol s =
     (builtin_symbol s)
 
 let xml_of_sort x = 
-  let to_string x = Ast.Ident (x, None) in
+  let to_string x = Ast.Ident (x, `Ambiguous) in
   let identify x = 
     add_xml_attrs (RenderingAttrs.keyword_attributes `MathML) (to_string x)
   in
@@ -271,8 +272,7 @@ let pp_ast0 status t k =
     | Ast.Sort sort -> aux_sort sort
     | Ast.Num _
     | Ast.Symbol _
-    | Ast.Ident (_, None) | Ast.Ident (_, Some [])
-    | Ast.Uri (_, None) | Ast.Uri (_, Some [])
+    | Ast.Ident _ 
     | Ast.Literal _
     | Ast.UserInput as leaf -> leaf
     | t -> NotationUtil.visit_ast ~special_k k t
@@ -599,11 +599,6 @@ let instantiate_level2 status env term =
     | Ast.LetRec (kind, definitions, body) ->
         Ast.LetRec (kind, List.map (aux_definition env) definitions,
           aux env body)
-    | Ast.Uri (name, None) -> Ast.Uri (name, None)
-    | Ast.Uri (name, Some substs) ->
-        Ast.Uri (name, Some (aux_substs env substs))
-    | Ast.Ident (name, Some substs) ->
-        Ast.Ident (name, Some (aux_substs env substs))
     | Ast.Meta (index, substs) -> Ast.Meta (index, aux_meta_substs env substs)
 
     | Ast.Implicit _
@@ -636,14 +631,14 @@ let instantiate_level2 status env term =
     List.map (fun (name, term) -> (name, aux env term)) substs
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
-    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
+    | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, None)
     | Ast.IdentVar name ->
        (match Env.lookup_string env name with
-           Env.Ident x -> Ast.Ident (x, None)
+           Env.Ident x -> Ast.Ident (x, `Ambiguous)
          | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
-    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)
+    | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, `Ambiguous)
     | Ast.Ascription (term, name) -> assert false
   and aux_magic env = function
     | Ast.Default (some_pattern, none_pattern) ->