(let final_s,final_env =
(List.fold_right
(fun (b,n,t) (s,env) ->
- let (acic,_,_,ids_to_inner_sorts) =
+ let (acic,_,_,ids_to_inner_sorts,_) =
Cic2acic.acic_of_cic_env metasenv env t
in
[< s ;
X.xml_nempty
(match b with
- ProofEngine.Definition -> "Definition"
- | ProofEngine.Declaration -> "Declaration"
+ ProofEngine.Definition -> "Def"
+ | ProofEngine.Declaration -> "Decl"
) ["name",(match n with Cic.Name n -> n | _ -> assert false)]
(Cic2Xml.print_term
(UriManager.uri_of_string "cic:/dummy.con")
) context ([<>],[])
)
in
- let (acic,_,_,ids_to_inner_sorts) =
+ let (acic,_,_,ids_to_inner_sorts,_) =
Cic2acic.acic_of_cic_env metasenv final_env goal
in
[< final_s ;