diff options
Diffstat (limited to 'plugins/xml/acic2Xml.ml4')
| -rw-r--r-- | plugins/xml/acic2Xml.ml4 | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4 index c03b13b5a..34bb1d51f 100644 --- a/plugins/xml/acic2Xml.ml4 +++ b/plugins/xml/acic2Xml.ml4 @@ -37,7 +37,7 @@ let print_term ids_to_inner_sorts = A.ARel (id,n,idref,b) -> let sort = Hashtbl.find ids_to_inner_sorts id in X.xml_empty "REL" - ["value",(string_of_int n) ; "binder",(N.string_of_id b) ; + ["value",(string_of_int n) ; "binder",(N.Id.to_string b) ; "id",id ; "idref",idref; "sort",sort] | A.AVar (id,uri) -> let sort = Hashtbl.find ids_to_inner_sorts id in @@ -71,7 +71,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("type",sort):: match binder with Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "decl" attrs (aux s) ; i >] ) [< >] prods ; @@ -96,7 +96,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("type",sort):: match binder with Names.Anonymous -> [] - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "decl" attrs (aux s) ; i >] ) [< >] lambdas ; @@ -115,7 +115,7 @@ let print_term ids_to_inner_sorts = ("id",id)::("sort",sort):: match binder with Names.Anonymous -> assert false - | Names.Name b -> ["binder",Names.string_of_id b] + | Names.Name b -> ["binder",Names.Id.to_string b] in [< X.xml_nempty "def" attrs (aux s) ; i >] ) [< >] letins ; @@ -161,7 +161,7 @@ let print_term ids_to_inner_sorts = (fun i (id,fi,ai,ti,bi) -> [< i ; X.xml_nempty "FixFunction" - ["id",id ; "name", (Names.string_of_id fi) ; + ["id",id ; "name", (Names.Id.to_string fi) ; "recIndex", (string_of_int ai)] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] @@ -177,7 +177,7 @@ let print_term ids_to_inner_sorts = (fun i (id,fi,ti,bi) -> [< i ; X.xml_nempty "CofixFunction" - ["id",id ; "name", Names.string_of_id fi] + ["id",id ; "name", Names.Id.to_string fi] [< X.xml_nempty "type" [] [< aux ti >] ; X.xml_nempty "body" [] [< aux bi >] >] @@ -229,11 +229,11 @@ let print_object uri ids_to_inner_sorts = [< (match t with n,A.Decl t -> X.xml_nempty "Decl" - ["id",hid;"name",Names.string_of_id n] + ["id",hid;"name",Names.Id.to_string n] (print_term ids_to_inner_sorts t) | n,A.Def (t,_) -> X.xml_nempty "Def" - ["id",hid;"name",Names.string_of_id n] + ["id",hid;"name",Names.Id.to_string n] (print_term ids_to_inner_sorts t) ) ; i @@ -315,7 +315,7 @@ let print_object uri ids_to_inner_sorts = (fun i (id,typename,finite,arity,cons) -> [< i ; X.xml_nempty "InductiveType" - ["id",id ; "name",Names.string_of_id typename ; + ["id",id ; "name",Names.Id.to_string typename ; "inductive",(string_of_bool finite) ] [< X.xml_nempty "arity" [] @@ -324,7 +324,7 @@ let print_object uri ids_to_inner_sorts = (fun i (name,lc) -> [< i ; X.xml_nempty "Constructor" - ["name",Names.string_of_id name] + ["name",Names.Id.to_string name] (print_term ids_to_inner_sorts lc) >]) [<>] cons ) |