- if not b then
- failwith "Wrong proof";
- (* TODO Zack [] probably wrong *)
- let obj =
- Cic.Constant ((UriManager.name_of_uri uri), (Some bo),ty,[])
- in
- let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
- CicEnvironment.add_type_checked_term uri (obj, ugraph);
- MetadataDb.index_constant ~dbd
- ~owner:(Helm_registry.get "matita.owner") ~uri ~body:(Some bo) ~ty;
- proof_handler.MatitaTypes.set_proof None;
- (MatitaMathView.proof_viewer_instance ())#unload;
- (* TODO Zack a lot more to be done here:
- * - save object to disk in xml format
- * - register uri to the getter
- * - save universe file *)
- Some `Command
+ if not b then failwith "Wrong proof";
+ add_constant_to_world ~dbd ~uri ~body:bo ~ty ~ugraph ();
+ currentProof#abort ();
+ (match mathViewer with None -> () | Some v -> v#unload ());
+ New_state Command