+ | TacticAst.Command (TacticAst.Qed name_opt) ->
+ (* TODO Zack this function probably should not simply fail with
+ * Failure, but rather raise some more meaningful exception *)
+ if not (proof_handler.MatitaTypes.has_proof ()) then assert false;
+ let proof = proof_handler.MatitaTypes.get_proof () in
+ (match name_opt with
+ | None -> ()
+ | Some name -> proof#set_uri (uri name));
+ let (uri, metasenv, bo, ty) = proof#proof in
+ let uri = MatitaTypes.unopt_uri uri in
+ if metasenv <> [] then failwith "Proof not completed";
+ let proved_ty = CicTypeChecker.type_of_aux' [] [] bo in
+ if not (CicReduction.are_convertible [] proved_ty ty) then
+ failwith "Wrong proof";
+ (* TODO Zack [] probably wrong *)
+ CicEnvironment.add_type_checked_term uri
+ (Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+ proof_handler.MatitaTypes.set_proof None;
+ (* TODO Zack a lot more to be done here:
+ * - save object to disk in xml format
+ * - collect metadata
+ * - register uri to the getter *)
+ Some `Command