match binding with
(Some (n,(Cic.Def t as b)) as entry)
| (Some (n,(Cic.Decl t as b)) as entry) ->
- let acic = acic_of_cic_context context t in
+ let acic = acic_of_cic_context context t None in
[< s ;
X.xml_nempty
(match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
) context ([<>],[])
)
in
- let acic = acic_of_cic_context context goal in
+ let acic = acic_of_cic_context context goal None in
X.xml_nempty "Sequent" ["no",string_of_int metano]
[< final_s ;
Xml.xml_nempty "Goal" []