diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-23 15:11:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-23 16:02:45 +0200 |
| commit | 4cb05fc1afaf938d1b36e0c00226ff173e2d8f22 (patch) | |
| tree | 0dc9a8c849bf11fa1177748b93c5542a3a4886fc /proofs/proof.ml | |
| parent | 6c5cf09f2436a2f5eacc3a58e2ea02fe09abe0b0 (diff) | |
Evd.future_goals: forgot to revert the list in two places.
Diffstat (limited to 'proofs/proof.ml')
| -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 24fdc41da..d00618be0 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 |