From e86b6558ab027704f2081b64dd68ac98a3b39736 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 15 Feb 2016 20:49:26 +0100
Subject: [PATCH] Add reflexivity for equality to the uPred hint DB.

---
 algebra/upred.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 465cfb505..8080cab98 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -982,5 +982,5 @@ Hint Resolve and_intro and_elim_l' and_elim_r' : I.
 Hint Resolve always_mono : I.
 Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
 Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl : I.
+Hint Immediate iff_refl eq_refl : I.
 End uPred.
-- 
GitLab