From eddfc6459c679e4d3f0c2f6c021822a137510320 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 1 Jul 2016 23:33:59 +0200
Subject: [PATCH] Use ndot_ne_disjoint more eager so it expands definitions.

---
 theories/tactics.v | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index ca64d1e9..ce5a3b95 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -412,10 +412,11 @@ Tactic Notation "feed" "destruct" constr(H) "as" simple_intropattern(IP) :=
 It will search for the first subterm of the goal matching [pat], and then call [tac]
 with that subterm. *)
 Ltac find_pat pat tac :=
-  match goal with |- context [?x] =>
-                  unify pat x with typeclass_instances;
-                  tryif tac x then idtac else fail 2
-end.
+  match goal with
+  |- context [?x] =>
+      unify pat x with typeclass_instances;
+      tryif tac x then idtac else fail 2
+  end.
 
 (** Coq's [firstorder] tactic fails or loops on rather small goals already. In 
 particular, on those generated by the tactic [unfold_elem_ofs] which is used
-- 
GitLab