From 667dd52bd039a96f896b81533b0aaafe98b9f8de Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 2 Sep 2020 23:26:39 +0200
Subject: compat Coq < 8.10

---
 mathcomp/ssreflect/bigop.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index ee3aedb..405ee08 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1509,7 +1509,11 @@ Lemma bigD1_ord n j (P : pred 'I_n) F :
     = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i).
 Proof.
 move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=.
-  by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT.
+  (** Coq >= 8.10 *)
+  (* by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. *)
+  (** Coq >= 8.7 *)
+  congr (_ * _); apply: eq_bigl => i.
+  by rewrite liftK eq_sym eqxx neq_lift ?andbT.
 by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF.
 Qed.
 
-- 
cgit v1.2.3