From 97ddb1f194e477865ddad6bd878b26f77f2103aa Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Nov 2016 13:23:39 +0100
Subject: [PATCH] Change order of eassumption and reflexivity in fast_done

This has bothered me repeatedly in proofs, now I finally got around to fix it at the source
---
 prelude/tactics.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/prelude/tactics.v b/prelude/tactics.v
index 08cb953fe..6c9bb2693 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -35,9 +35,12 @@ declarations as the ones above. *)
 Tactic Notation "intuition" := intuition auto.
 
 (* [done] can get slow as it calls "trivial". [fast_done] can solve way less
-   goals, but it will also always finish quickly. *)
+   goals, but it will also always finish quickly.
+   We do 'reflexivity' last because for goals of the form ?x = y, if
+   we have x = y in the context, we will typically want to use the
+   assumption and not reflexivity *)
 Ltac fast_done :=
-  solve [ reflexivity | eassumption | symmetry; eassumption ].
+  solve [ eassumption | symmetry; eassumption | reflexivity ].
 Tactic Notation "fast_by" tactic(tac) :=
   tac; fast_done.
 
-- 
GitLab