- let proofterm = Inference.build_proof_term newproof in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm)
- initialstatus
+ if newmeta != maxm then
+ begin
+ let opengoal = Cic.Meta(maxm,irl) in
+ let proofterm =
+ Inference.build_proof_term ~noproof:opengoal newproof in
+ prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context));
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv));
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
+ end
+ else raise (ProofEngineTypes.Fail (lazy "no progress"))