From c30500ff4db56b6b3ad77dad811e3da766b26e19 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Mon, 29 Apr 2019 23:18:35 +0200
Subject: Fix compatibility for #237

- reprove rather than specialize `Some_inj` to allow for redefinition
of `nonPropType` in `mathcomp.ssreflect.ssreflect`
- retarget finmap CI to coq-9995-compatibility
---
 .gitlab-ci.yml              | 8 ++++++++
 mathcomp/ssreflect/ssrfun.v | 3 ++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3eae6fa..b88a782 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -294,21 +294,29 @@ ci-bigenough-dev:
 ci-finmap-8.7:
   extends: .ci-finmap
   variables:
+    CONTRIB_URL: "https://github.com/ggonthier/finmap.git"
+    CONTRIB_VERSION: coq-9995-compatibility
     COQ_VERSION: "8.7"
 
 ci-finmap-8.8:
   extends: .ci-finmap
   variables:
+    CONTRIB_URL: "https://github.com/ggonthier/finmap.git"
+    CONTRIB_VERSION: coq-9995-compatibility
     COQ_VERSION: "8.8"
 
 ci-finmap-8.9:
   extends: .ci-finmap
   variables:
+    CONTRIB_URL: "https://github.com/ggonthier/finmap.git"
+    CONTRIB_VERSION: coq-9995-compatibility
     COQ_VERSION: "8.9"
 
 ci-finmap-dev:
   extends: .ci-finmap
   variables:
+    CONTRIB_URL: "https://github.com/ggonthier/finmap.git"
+    CONTRIB_VERSION: coq-9995-compatibility
     COQ_VERSION: "dev"
 
 ################
diff --git a/mathcomp/ssreflect/ssrfun.v b/mathcomp/ssreflect/ssrfun.v
index ed18941..1c1b557 100644
--- a/mathcomp/ssreflect/ssrfun.v
+++ b/mathcomp/ssreflect/ssrfun.v
@@ -2,4 +2,5 @@ From mathcomp Require Import ssreflect.
 From Coq Require Export ssrfun.
 From mathcomp Require Export ssrnotations.
 
-Definition Some_inj {T : nonPropType} := @Some_inj T.
+Lemma Some_inj {T : nonPropType} : injective (@Some T).
+Proof. by move=> x y []. Qed.
-- 
cgit v1.2.3