diff options
| author | Arnaud Spiwack | 2014-10-23 15:11:52 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-10-23 16:02:45 +0200 |
| commit | 4cb05fc1afaf938d1b36e0c00226ff173e2d8f22 (patch) | |
| tree | 0dc9a8c849bf11fa1177748b93c5542a3a4886fc | |
| parent | 6c5cf09f2436a2f5eacc3a58e2ea02fe09abe0b0 (diff) | |
Evd.future_goals: forgot to revert the list in two places.
| -rw-r--r-- | proofs/proof.ml | 2 | ||||
| -rw-r--r-- | toplevel/classes.ml | 2 |
2 files changed, 2 insertions, 2 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 diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 60da19c186..d8b2ed0e75 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -297,7 +297,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro the pretyping after the proof has opened. As a consequence, we use the low-level primitives to code the refinement manually.*) - let gls = Evd.future_goals evm in + let gls = List.rev (Evd.future_goals evm) in let evm = Evd.reset_future_goals evm in Lemmas.start_proof id kind evm termtype (Lemmas.mk_hook |