- try
- txt_of_cic_object
- ~map_unicode_to_tex 78 style ?flavour prefix
- (fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri))
+ try
+(* FG: for now the explicit variables must be discharged *)
+ let do_it obj = txt_of_cic_object ~map_unicode_to_tex 78 style ?flavour prefix obj in
+ match CicDischarge.discharge_uri (discharge_uri style) uri with
+ | C.InductiveDefinition _ as obj', false ->
+ let uri' = discharge_uri style uri in
+ TC.typecheck_obj uri' obj';
+ (* we loose the sharing in this case *)
+ let obj'', _ = E.get_obj Un.default_ugraph uri' in
+ let s = do_it obj'' in begin E.remove_obj uri'; s end
+ | obj, _ -> do_it obj