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