aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Util/WordUtil.v2
1 files changed, 1 insertions, 1 deletions
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