Symbol of string option * string * subst option * string option
(* h:xref, name, subst, definitionURL *)
| LocalVar of (string option) * string (* h:xref, name *)
Symbol of string option * string * subst option * string option
(* h:xref, name, subst, definitionURL *)
| LocalVar of (string option) * string (* h:xref, name *)
| Num of string option * string (* h:xref, value *)
| Appl of string option * cexpr list (* h:xref, args *)
| Binder of string option * string * decl * cexpr
| Num of string option * string (* h:xref, value *)
| Appl of string option * cexpr list (* h:xref, args *)
| Binder of string option * string * decl * cexpr
def = string * cexpr (* name, body *)
and
subst = (UriManager.uri * cexpr) list
def = string * cexpr (* name, body *)
and
subst = (UriManager.uri * cexpr) list
| C.AVar (id,uri,subst) ->
Symbol (Some id, UriManager.name_of_uri uri,
make_subst subst, Some (UriManager.string_of_uri uri))
| C.AVar (id,uri,subst) ->
Symbol (Some id, UriManager.name_of_uri uri,
make_subst subst, Some (UriManager.string_of_uri uri))
- | C.AMeta (id,n,l) -> Meta (Some id,("?" ^ (string_of_int n)))
+ | C.AMeta (id,n,l) ->
+ let l' =
+ List.rev_map
+ (function
+ None -> None
+ | Some t -> Some (acic2cexpr t)
+ ) l
+ in
+ Meta (Some id,("?" ^ (string_of_int n)),l')
| C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
| C.AImplicit _ -> raise NotImplemented
| C.AProd (id,n,s,t) ->
| C.ASort (id,s) -> Symbol (Some id,string_of_sort s,None,None)
| C.AImplicit _ -> raise NotImplemented
| C.AProd (id,n,s,t) ->