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 ;
| None ->
(* Invariant: "" is never looked up *)
[< s ; X.xml_empty "Hidden" [] >], (None::context), ""::idrefs
+ | Some (_,Cic.Def (_,Some _)) -> assert false
) context ([<>],[],[])
)
in