From 9d7640c04b81f643a6ec0f9feb3dfeed7f0e6702 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 May 2019 08:06:44 +0200
Subject: [PATCH] Revert "`RelDecision` instance for `flip`, and make `flip` tc
 opaque to avoid loops due to eager unification."

This reverts commit b81aa3aaa4a4b1cf31a6f03eeb7809012b516240.
---
 theories/base.v      | 7 +------
 theories/decidable.v | 6 +-----
 2 files changed, 2 insertions(+), 11 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 4f9c20a6..86d98c17 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -505,12 +505,7 @@ Arguments id _ _ / : assert.
 Arguments compose _ _ _ _ _ _ / : assert.
 Arguments flip _ _ _ _ _ _ / : assert.
 Arguments const _ _ _ _ / : assert.
-Typeclasses Transparent id compose const.
-
-(** Make sure that [flip] is type class opaque, otherwise one gets loops due to
-instance involving [flip], e.g. [RelDecision R → RelDecision (flip R)] could be
-used indefinitely. *)
-Typeclasses Opaque flip.
+Typeclasses Transparent id compose flip const.
 
 Definition fun_map {A A' B B'} (f: A' → A) (g: B → B') (h : A → B) : A' → B' :=
   g ∘ h ∘ f.
diff --git a/theories/decidable.v b/theories/decidable.v
index 062dd1dc..c78d72a6 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -135,7 +135,7 @@ Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
   dexist (`x) p = x.
 Proof. apply dsig_eq; reflexivity. Qed.
 
-(** * Instances of [Decision] *)
+(** * Instances of Decision *)
 (** Instances of [Decision] for operators of propositional logic. *)
 Instance True_dec: Decision True := left I.
 Instance False_dec: Decision False := right (False_rect False).
@@ -192,7 +192,3 @@ Proof. destruct (decide Q); tauto. Qed.
 Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
   `{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
 Solve Obligations with firstorder congruence.
-
-(** * Instances of [RelDecision] *)
-Instance flip_dec {A} (R : relation A) `{!RelDecision R} :
-  RelDecision (flip R) := λ x y, decide_rel R y x.
-- 
GitLab