+ let cic_proof,newmetasenv,proof_menv,ty, ug =
+ prerr_endline "type checking ... (old) ";
+(* let old_ty, oldug = *)
+(* CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph *)
+(* in*)
+ let cic_proof_new,new_ty,newmetasenv_new,newug =
+ try
+ (*
+ prerr_endline "refining ... (new) ";
+ CicRefine.type_of_aux'
+ newmetasenv_new context cic_proof_new ugraph*)
+ let ty,ug =
+ prerr_endline "typechecking ... (new) ";
+ CicTypeChecker.type_of_aux'
+ newmetasenv_new context cic_proof_new ugraph
+ in
+ cic_proof_new, ty, newmetasenv_new, ug
+ with
+ | CicTypeChecker.TypeCheckerFailure s ->
+ prerr_endline "FAILURE IN TYPECHECKING";
+ prerr_endline (Lazy.force s);
+ assert false
+ | CicRefine.RefineFailure s
+ | CicRefine.Uncertain s
+ | CicRefine.AssertFailure s ->
+ prerr_endline "FAILURE IN REFINE";
+ prerr_endline (Lazy.force s);
+ interactive_comparison context cic_proof_new cic_proof;
+ assert false
+ in
+(*
+ prerr_endline "check unif ... (old vs new) ";
+ (try
+ ignore(CicUnification.fo_unif
+ newmetasenv_new context cic_proof_new cic_proof CicUniv.empty_ugraph)
+ with CicUnification.UnificationFailure _ ->
+ prerr_endline "WARNING, new and old proofs are not unifiable");
+ prerr_endline "unif ... (new) ";
+ let subst, newmetasenv_new, newug =
+ CicUnification.fo_unif
+ newmetasenv_new context new_ty type_of_goal newug
+ in
+ if subst <> [] then
+ prerr_endline "UNIF SERVE ################################";
+*)
+ let subst = [] in
+ if List.length newmetasenv_new <> 0 then
+ prerr_endline
+ ("Some METAS are still open: " ^ CicMetaSubst.ppmetasenv
+ [] newmetasenv_new);
+ (CicMetaSubst.apply_subst subst cic_proof_new),
+ newmetasenv_new,
+ (CicMetaSubst.apply_subst_metasenv subst newmetasenv_new),
+ (CicMetaSubst.apply_subst subst new_ty),
+ newug
+(* cic_proof,newmetasenv,proof_menv,oldty,oldug*)