- name, List.map (fun (id,con) -> (id,deannotate_term con)) conjs,
+ name,
+ List.map
+ (function
+ (id,acontext,con) ->
+ let context =
+ List.map
+ (function
+ Some (n,(C.ADef at)) -> Some (n,(C.Def (deannotate_term at)))
+ | Some (n,(C.ADecl at)) ->Some (n,(C.Decl (deannotate_term at)))
+ | None -> None) acontext
+ in
+ (id,context, deannotate_term con)
+ ) conjs,