From 4cb05fc1afaf938d1b36e0c00226ff173e2d8f22 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Thu, 23 Oct 2014 15:11:52 +0200
Subject: Evd.future_goals: forgot to revert the list in two places.

---
 proofs/proof.ml     | 2 +-
 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
-- 
cgit v1.2.3