aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/class_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9f6624889..f386e804e 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -983,7 +983,7 @@ module Search = struct
(str "leaking evar " ++ int (Evar.repr ev) ++
spc () ++ pr_ev evm' ev);
acc && okev) evm' true);
- let evm' = Evd.restore_future_goals evm' (shelved @ fgoals) pgoal in
+ let evm' = Evd.restore_future_goals evm' (shelved @ fgoals, pgoal) in
let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
Some evm'
else raise Not_found