- try
- 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*)
+ let cic_proof,newmetasenv,proof_menv,ty, ug =
+ prerr_endline "type checking ... (old) ";
+ let _old_ty, _oldug =
+ try
+ CicTypeChecker.type_of_aux' newmetasenv context cic_proof ugraph
+ with
+ CicTypeChecker.TypeCheckerFailure s ->
+ prerr_endline "THE *OLD* PROOF DOESN'T TYPECHECK!!!";
+ prerr_endline (Lazy.force s);
+ Cic.Implicit None, CicUniv.empty_ugraph