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
---
 test-suite/ssr/under.v | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index c12491138a..0312b9c733 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -313,8 +313,7 @@ Qed.
 End TestGeneric2.
 
 Section TestPreOrder.
-(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950
-   but without needing to do [rewrite UnderE] manually. *)
+(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950 *)
 
 Require Import Morphisms.
 
@@ -330,7 +329,7 @@ Parameter leq_mul :
 
 Local Notation "+%N" := addn (at level 0, only parsing).
 
-(** Context lemma (could *)
+(** Context lemma *)
 Lemma leq'_big : forall I (F G : I -> nat) (r : seq I),
     (forall i : I, leq' (F i) (G i)) ->
     (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)).
@@ -370,8 +369,10 @@ have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n).
 
 under leq'_big => i.
 {
-  (* The "magic" is here: instantiate the evar with the bound "3 + n" *)
-  rewrite lem ?ltn_ord //. over.
+  rewrite UnderE.
+
+  (* instantiate the evar with the bound "3 + n" *)
+  apply: lem; exact: ltn_ord.
 }
 cbv beta.
 
-- 
cgit v1.2.3