1 files changed, 4 insertions, 1 deletions
diff --git a/src/Util/Relations.v b/src/Util/Relations.v
index 4926bd74c..8ab045cfe 100644
--- a/src/Util/Relations.v
+++ b/src/Util/Relations.v
@@ -47,4 +47,7 @@ Proof.
            | _ => progress (cbv [fst snd] in * )
            | _ => solve[eauto]
          end.
-Qed.
-\ No newline at end of file
+Qed.
+
+Global Instance eq_eta_Reflexive {T} : Reflexive (fun x y : T => x = y) | 1
+  := eq_Reflexive.