Add reflexivity for equality to the uPred hint DB.

e86b6558 · Robbert Krebbers · 824257bc · e86b6558
Commit e86b6558 authored Feb 15, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 1 addition and 1 deletion

algebra/upred.v algebra/upred.v +1 -1

No files found.
--- 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.