- let newstatus =
- let cic_proof,newmetasenv,proof_menv,ty, ug =
- 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 "THE PROOF DOESN'T TYPECHECK!!!";
- 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);
- assert false
- in
- if List.length newmetasenv_new <> 0 then
- prerr_endline
- ("Some METAS are still open: "(* ^ CicMetaSubst.ppmetasenv
- [] newmetasenv_new*));
- cic_proof_new, newmetasenv_new, newmetasenv_new,new_ty, newug
- (* THE OLD PROOF: cic_proof,newmetasenv,proof_menv,oldty,oldug *)
- in
- prerr_endline "FINAL PROOF";
- prerr_endline (CicPp.pp cic_proof names);
- prerr_endline "ENDOFPROOFS";
- (*
- debug_print
- (lazy
- (Printf.sprintf
- "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n"
- (CicPp.pp type_of_goal names) (CicPp.pp ty names)
- (string_of_bool
- (fst (CicReduction.are_convertible
- context type_of_goal ty ug)))));
- *)
- let real_proof =
- ProofEngineReduction.replace
- ~equality:equality_for_replace
- ~what:[goal'] ~with_what:[cic_proof]
- ~where:meta_proof
+ let replaced_goal =
+ ProofEngineReduction.replace
+ ~what:side_effects ~with_what:side_effects_t
+ ~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
+ ~where:type_of_goal
+ in
+ let subst_side_effects,real_menv,_ =
+ let fail t s = raise (ProofEngineTypes.Fail (lazy (t^Lazy.force s))) in
+ let free_metas_menv =
+ List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas