diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 14 | ||||
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | proofs/refine.ml | 9 |
3 files changed, 15 insertions, 10 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index 1c3aed8fc2..7aea07d6f0 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -56,12 +56,18 @@ module V82 = struct be shelved. It must not appear as a future_goal, so the future goals are restored to their initial value after the evar is created. *) - let prev_future_goals = Evd.save_future_goals evars in let inst = EConstr.identity_subst_val hyps in - let (evars, evk) = - Evarutil.new_pure_evar ~src:(Loc.tag Evar_kinds.GoalEvar) ~typeclass_candidate:false ~identity:inst hyps evars concl + let evi = { Evd.evar_hyps = hyps; + Evd.evar_concl = concl; + Evd.evar_filter = Evd.Filter.identity; + Evd.evar_abstract_arguments = Evd.Abstraction.identity; + Evd.evar_body = Evd.Evar_empty; + Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); + Evd.evar_candidates = None; + Evd.evar_identity = Evd.Identity.make inst; + } in - let evars = Evd.restore_future_goals evars prev_future_goals in + let (evars, evk) = Evd.new_evar evars ~typeclass_candidate:false evi in let ev = EConstr.mkEvar (evk,inst) in (evk, ev, evars) diff --git a/proofs/proof.ml b/proofs/proof.ml index 38fcdd6e5f..c427c07b93 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -373,7 +373,7 @@ let run_tactic env tac pr = Proofview.tclEVARMAP >>= fun sigma -> (* Already solved goals are not to be counted as shelved. Nor are they to be marked as unresolvable. *) - let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) (Evd.save_future_goals sigma) in + let retrieved = Evd.filter_future_goals (Evd.is_undefined sigma) sigma in let retrieved,retrieved_given_up = Evd.extract_given_up_future_goals retrieved in (* Check that retrieved given up is empty *) if not (List.is_empty retrieved_given_up) then diff --git a/proofs/refine.ml b/proofs/refine.ml index a10bbcbdd4..8909b9639d 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -55,15 +55,14 @@ let generic_refine ~typecheck f gl = (* Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> - Proofview.tclEVARMAP >>= fun sigma -> + Proofview.tclEVARMAP >>= fun sigma' -> Proofview.V82.wrap_exceptions begin fun () -> - let evs = Evd.save_future_goals sigma in (* Redo the effects in sigma in the monad's env *) - let privates_csts = Evd.eval_side_effects sigma in + let privates_csts = Evd.eval_side_effects sigma' in let env = Safe_typing.push_private_constants env privates_csts.Evd.seff_private in (* Check that the introduced evars are well-typed *) let fold accu ev = typecheck_evar ev env accu in - let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in + let sigma = if typecheck then Evd.fold_future_goals fold sigma' else sigma' in (* Check that the refined term is typesafe *) let sigma = if typecheck then Typing.check env sigma c concl else sigma in (* Check that the goal itself does not appear in the refined term *) @@ -75,7 +74,7 @@ let generic_refine ~typecheck f gl = (* Restore the [future goals] state. *) let sigma = Evd.restore_future_goals sigma prev_future_goals in (* Select the goals *) - let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in + let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) sigma' in let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in (* Proceed to the refinement *) let sigma = match Proofview.Unsafe.advance sigma self with |