match i with
Some (n,Cic.Decl t) ->
print_name n ^ ":" ^ CicPp.pp t context ^ "\n", (Some n)::context
- | Some (n,Cic.Def t) ->
+ | Some (n,Cic.Def (t,None)) ->
print_name n ^ ":=" ^ CicPp.pp t context ^ "\n", (Some n)::context
| None ->
"_ ?= _\n", None::context
+ | Some (_,Cic.Def (_,Some _)) -> assert false
in
output^newoutput,context'
) ctx ("",[])
Hashtbl.add ids_to_hypotheses hid binding ;
incr hypotheses_seed ;
match binding with
- (Some (n,(Cic.Def t as b)) as entry)
+ (Some (n,(Cic.Def (t,None) as b)) as entry)
| (Some (n,(Cic.Decl t as b)) as entry) ->
let acic = acic_of_cic_context context idrefs t None in
[< s ;
X.xml_nempty
(match b with Cic.Decl _ -> "Decl" | Cic.Def _ -> "Def")
- ["name",(match n with Cic.Name n -> n | _ -> assert false);
- "id",hid]
+ [None,"name",(match n with Cic.Name n -> n | _ -> assert false);
+ None,"id",hid]
(Cic2Xml.print_term ~ids_to_inner_sorts acic)
>], (entry::context), (hid::idrefs)
| None ->
(* Invariant: "" is never looked up *)
[< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context ([<>],[],[])
)
in
let acic = acic_of_cic_context context final_idrefs goal None in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata ("<!DOCTYPE Sequent SYSTEM \"" ^ dtdname ^ "\">\n");
- X.xml_nempty "Sequent" ["no",string_of_int metano;"id",sequent_id]
+ X.xml_nempty "Sequent"
+ [None,"no",string_of_int metano;None,"id",sequent_id]
[< final_s ;
Xml.xml_nempty "Goal" []
(Cic2Xml.print_term ~ids_to_inner_sorts acic)