From ec2d1bc0d0f0447f8824def545697b8c05fcb670 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Fri, 27 Dec 2019 00:13:52 +0100
Subject: fix: Shorten ssrsetoid.v

* This patch is a quick fix that removes part of the features of coq/coq#10022,
  namely the ability to directly use setoid_rewrite with a (Under_rel)-tagged
  relation R. This just means we'll need to do an extra step [rewrite UnderE.]
  which was unnecessary with Coq 8.11+alpha.
* This PR stays backward-compatible w.r.t. Coq 8.10 and also keeps the salient
  feature of coq/coq#10022 (generalize under & over to any Reflexive relation).
* Related: coq-community/atbr#23
---
 plugins/ssr/ssrsetoid.v | 86 +------------------------------------------------
 1 file changed, 1 insertion(+), 85 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrsetoid.v b/plugins/ssr/ssrsetoid.v
index 609c9d5ab8..7c5cd135fe 100644
--- a/plugins/ssr/ssrsetoid.v
+++ b/plugins/ssr/ssrsetoid.v
@@ -18,9 +18,7 @@
  than [eq] or [iff], e.g. a [RewriteRelation], by doing:
  [Require Import ssreflect. Require Setoid.]
 
- This file's instances have priority 12 > other stdlib instances
- and each [Under_rel] instance comes with a [Hint Cut] directive
- (otherwise Ring_polynom.v won't compile because of unbounded search).
+ This file's instances have priority 12 > other stdlib instances.
 
  (Note: this file could be skipped when porting [under] to stdlib2.)
  *)
@@ -38,85 +36,3 @@ Instance compat_Reflexive :
     RelationClasses.Reflexive R ->
     ssrclasses.Reflexive R | 12.
 Proof. now trivial. Qed.
-
-(** Add instances so that ['Under[ F i ]] terms,
-    that is, [Under_rel T R (F i) (?G i)] terms,
-    can be manipulated with rewrite/setoid_rewrite with lemmas on [R].
-    Note that this requires that [R] is a [Prop] relation, otherwise
-    a [bool] relation may need to be "lifted": see the [TestPreOrder]
-    section in test-suite/ssr/under.v *)
-
-Instance Under_subrelation {A} (R : relation A) : subrelation R (Under_rel _ R) | 12.
-Proof. now rewrite Under_relE. Qed.
-
-(* see also Morphisms.trans_co_eq_inv_impl_morphism *)
-
-Instance Under_Reflexive {A} (R : relation A) :
-  RelationClasses.Reflexive R ->
-  RelationClasses.Reflexive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Reflexive Under_Reflexive] : typeclass_instances.
-
-(* These instances are a bit off-topic given that (Under_rel A R) will
-   typically be reflexive, to be able to trigger the [over] terminator
-
-Instance under_Irreflexive {A} (R : relation A) :
-  RelationClasses.Irreflexive R ->
-  RelationClasses.Irreflexive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Irreflexive Under_Irreflexive] : typeclass_instances.
-
-Instance under_Asymmetric {A} (R : relation A) :
-  RelationClasses.Asymmetric R ->
-  RelationClasses.Asymmetric (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Asymmetric Under_Asymmetric] : typeclass_instances.
-
-Instance under_StrictOrder {A} (R : relation A) :
-  RelationClasses.StrictOrder R ->
-  RelationClasses.StrictOrder (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Strictorder Under_Strictorder] : typeclass_instances.
- *)
-
-Instance Under_Symmetric {A} (R : relation A) :
-  RelationClasses.Symmetric R ->
-  RelationClasses.Symmetric (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Symmetric Under_Symmetric] : typeclass_instances.
-
-Instance Under_Transitive {A} (R : relation A) :
-  RelationClasses.Transitive R ->
-  RelationClasses.Transitive (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Transitive Under_Transitive] : typeclass_instances.
-
-Instance Under_PreOrder {A} (R : relation A) :
-  RelationClasses.PreOrder R ->
-  RelationClasses.PreOrder (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_PreOrder Under_PreOrder] : typeclass_instances.
-
-Instance Under_PER {A} (R : relation A) :
-  RelationClasses.PER R ->
-  RelationClasses.PER (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_PER Under_PER] : typeclass_instances.
-
-Instance Under_Equivalence {A} (R : relation A) :
-  RelationClasses.Equivalence R ->
-  RelationClasses.Equivalence (Under_rel.Under_rel A R) | 12.
-Proof. now rewrite Under_rel.Under_relE. Qed.
-
-Hint Cut [_* Under_Equivalence Under_Equivalence] : typeclass_instances.
-
-(* Don't handle Antisymmetric and PartialOrder classes for now,
-   as these classes depend on two relation symbols... *)
-- 
cgit v1.2.3