(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
(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
| 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
| 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 _
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) ->