From 3c4ff8fe8d2154addcf440690d315c58a529c1f6 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 21 Jan 2017 18:51:28 -0500
Subject: Fix a missing qualification

---
 src/Util/WordUtil.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src')

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index d36292f95..0e3f6a168 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1220,7 +1220,7 @@ Proof.
     repeat first [ progress simpl
                  | intro
                  | congruence
-                 | exists eq_refl
+                 | exists Logic.eq_refl
                  | progress destruct_head ex
                  | progress destruct_head bool
                  | progress subst
-- 
cgit v1.2.3