aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/equality.ml2
1 files changed, 1 insertions, 1 deletions
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 *)