diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/proof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml index 24fdc41dac..d00618be01 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -321,7 +321,7 @@ let run_tactic env tac pr = let (_,tacticced_proofview,(status,to_shelve,give_up)) = Proofview.apply env tac sp in let shelf = let sigma = Proofview.return tacticced_proofview in - let pre_shelf = pr.shelf@(Evd.future_goals sigma)@to_shelve in + let pre_shelf = pr.shelf@(List.rev (Evd.future_goals sigma))@to_shelve in (* avoid already to count already solved goals as shelved. *) List.filter (fun g -> Evd.is_undefined sigma g) pre_shelf in |