From 5a0d3395cd972393eaa7859f47a738cc99ea55c6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 6 May 2015 12:35:42 +0200
Subject: Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order
 after patch for #4214 on subst needed to be repeated (see 857e82b2ca0d1).

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f2860a2300..c5b87761d8 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1681,7 +1681,7 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
       with Constr_matching.PatternMatchingFailure -> None
     in
     let hyps = Proofview.Goal.hyps gl in
-    List.map_filter test hyps
+    List.rev (List.map_filter test hyps)
   in
 
   (* Second step: treat equations *)
-- 
cgit v1.2.3