From ce94aec9d6604b41217529525b7a73850c530e7b Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Wed, 30 Sep 2020 17:25:56 +0100
Subject: Tweak Coq proof to avoid incompatibility with Iris (in the previous
 proof script the intuition tactic found a strange proof involving a
 type-level dependent pair that imposed an unnecessary universe constraint,
 this doesn't)

---
 lib/coq/Operators_mwords.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Operators_mwords.v b/lib/coq/Operators_mwords.v
index 9b38c95c..bfbf6549 100644
--- a/lib/coq/Operators_mwords.v
+++ b/lib/coq/Operators_mwords.v
@@ -528,7 +528,7 @@ destruct n.
   compute. intuition.
 * simpl in *. destruct (weq v w).
   + subst. rewrite weqb_eq; tauto.
-  + rewrite weqb_ne; auto. intuition.
+  + rewrite weqb_ne; auto. split; congruence.
 * destruct v.
 Qed.
 
-- 
cgit v1.2.3