From f1f45de3c19f93c3a1a3a432dcb79049589cc121 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 19 Nov 2015 16:18:51 +0100
Subject: [PATCH] COFE on type with leibniz equality.
---
theories/base.v | 2 ++
1 file changed, 2 insertions(+)
diff --git a/theories/base.v b/theories/base.v
index 497e040c..30ec9466 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -194,6 +194,8 @@ Ltac unfold_leibniz := repeat
setoid_rewrite <-(leibniz_equiv (A:=A))
end.
+Definition equivL {A} : Equiv A := (=).
+
(** A [Params f n] instance forces the setoid rewriting mechanism not to
rewrite in the first [n] arguments of the function [f]. We will declare such
instances for all operational type classes in this development. *)
--
GitLab