From c579b46cfbaafae107d43f003a307ceec7c8057f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 5 Sep 2019 20:15:37 +0200
Subject: [PATCH] Avoid use of `solve_proper`.
Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
instead of the version of std++. The version in std++ can inherently
not solve this, so I changed it into a manual proof.
---
theories/fin_sets.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/fin_sets.v b/theories/fin_sets.v
index cab9674..e71f698 100644
--- a/theories/fin_sets.v
+++ b/theories/fin_sets.v
@@ -401,7 +401,7 @@ Section infinite.
(** Properties about the [fresh] operation on finite sets *)
Global Instance fresh_proper: Proper ((≡@{C}) ==> (=)) fresh.
- Proof. unfold fresh, set_fresh. solve_proper. Qed.
+ Proof. unfold fresh, set_fresh. by intros X1 X2 ->. Qed.
Lemma is_fresh X : fresh X ∉ X.
Proof.
--
GitLab