diff options
| author | Maxime Dénès | 2018-03-09 10:24:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-09 10:24:18 +0100 |
| commit | fd852113ea205720a9394c27989acaac408f7643 (patch) | |
| tree | f3cb2d7b11c3bb161139ac81232c343c980c45e0 /tactics | |
| parent | 49dd2bddc03ce64707cb93d450127152ad6eece6 (diff) | |
| parent | e7bf157c6af0d7f65b0611f7dfa9c00d5e1e7a83 (diff) | |
Merge PR #6328: Fix #6313: lost goals in nested ltac in refine
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 9f66248897..0260460e64 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -966,14 +966,15 @@ module Search = struct top_sort evm' goals else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) in - let fgoals = Evd.future_goals evm in - let pgoal = Evd.principal_future_goal evm in + let fgoals = Evd.save_future_goals evm in let _, pv = Proofview.init evm' [] in let pv = Proofview.unshelve goals pv in try let (), pv', (unsafe, shelved, gaveup), _ = Proofview.apply env tac pv in + if not (List.is_empty gaveup) then + CErrors.anomaly (Pp.str "run_on_evars not assumed to apply tactics generating given up goals."); if Proofview.finished pv' then let evm' = Proofview.return pv' in assert(Evd.fold_undefined (fun ev _ acc -> @@ -983,7 +984,8 @@ 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 fgoals = Evd.shelve_on_future_goals shelved fgoals in + let evm' = Evd.restore_future_goals evm' fgoals in let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in Some evm' else raise Not_found |