) [< >] lambdas ;
X.xml_nempty "target" [] (aux t)
>]
- | C.ALetIn (xid,C.Anonymous,s,t) ->
+ | C.ALetIn (xid,C.Anonymous,s,ty,t) ->
assert false
- | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ | C.ALetIn (last_id,C.Name _,_,_,_) as letins ->
let rec eat_letins =
function
- C.ALetIn (id,n,s,t) ->
+ C.ALetIn (id,n,s,ty,t) ->
let letins,t' = eat_letins t in
- (id,n,s)::letins,t'
+ (id,n,s,ty)::letins,t'
| t -> [],t
in
let letins,t = eat_letins letins in
let sort = find_sort "sort" last_id in
X.xml_nempty "LETIN" sort
[< List.fold_left
- (fun i (id,binder,s) ->
+ (fun i (id,binder,s,ty) ->
let sort = find_sort "sort" id in
let attrs =
sort @ ((None,"id",id)::
C.Anonymous -> []
| C.Name b -> [None,"binder",b])
in
- [< i ; X.xml_nempty "def" attrs (aux s) >]
+ [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >]
) [< >] letins ;
X.xml_nempty "target" [] (aux t)
>]
[None,"id",hid;None,"name",n']
| C.Anonymous -> [None,"id",hid])
(print_term ?ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
+ | Some (n,C.ADef (t,_)) ->
X.xml_nempty "Def"
(match n with
C.Name n' ->