diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-12-06 09:30:26 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-08 21:58:31 +0100 |
| commit | bfb393596b1df815a109c9c600b9a2b413561fcb (patch) | |
| tree | 57a79325475f1df46c5f0ba07ef194e9eb9f20c7 /proofs | |
| parent | e508aec3a90aca93c188c54b707d19114ef5ff83 (diff) | |
Proof engine: using save_future_goal when relevant.
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/goal.ml | 5 | ||||
| -rw-r--r-- | proofs/refine.ml | 5 |
2 files changed, 4 insertions, 6 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml index e153aa277..ba7e458f3 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -62,8 +62,7 @@ module V82 = struct goals are restored to their initial value after the evar is created. *) let concl = EConstr.Unsafe.to_constr concl in - let prev_future_goals = Evd.future_goals evars in - let prev_principal_goal = Evd.principal_future_goal evars in + let prev_future_goals = Evd.save_future_goals evars in let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; @@ -74,7 +73,7 @@ module V82 = struct in let evi = Typeclasses.mark_unresolvable evi in let (evars, evk) = Evarutil.new_pure_evar_full evars evi in - let evars = Evd.restore_future_goals evars (prev_future_goals,prev_principal_goal) in + let evars = Evd.restore_future_goals evars prev_future_goals in let ctxt = Environ.named_context_of_val hyps in let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in let ev = EConstr.mkEvar (evk,inst) in diff --git a/proofs/refine.ml b/proofs/refine.ml index 39d77d983..b5578a187 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -78,8 +78,7 @@ let generic_refine ~typecheck f gl = let state = Proofview.Goal.state gl in (** Save the [future_goals] state to restore them after the refinement. *) - let prev_future_goals = Evd.future_goals sigma in - let prev_principal_goal = Evd.principal_future_goal sigma in + let prev_future_goals = Evd.save_future_goals sigma in (** Create the refinement term *) Proofview.Unsafe.tclEVARS (Evd.reset_future_goals sigma) >>= fun () -> f >>= fun (v, c) -> @@ -119,7 +118,7 @@ let generic_refine ~typecheck f gl = | Some id -> Evd.rename evk id sigma in (** Restore the [future goals] state. *) - let sigma = Evd.restore_future_goals sigma (prev_future_goals,prev_principal_goal) in + let sigma = Evd.restore_future_goals sigma prev_future_goals in (** Select the goals *) let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in |