diff options
| author | Hugo Herbelin | 2017-12-06 08:58:50 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-08 21:58:26 +0100 |
| commit | d2c50bb29df8f0b23f7ee498abeda43a672fc688 (patch) | |
| tree | 127379b1d724f5b7b76f2b0a48a942cc7552f35e /proofs/refine.ml | |
| parent | 866bad4e9cdaa6ff4419840f8c9980f770873176 (diff) | |
Proof engine: consider the pair principal and future goals as an entity.
Diffstat (limited to 'proofs/refine.ml')
| -rw-r--r-- | proofs/refine.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/refine.ml b/proofs/refine.ml index 50fd1c4722..39d77d983f 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -119,7 +119,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,prev_principal_goal) 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 |