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
---
 mathcomp/ssreflect/ssrfun.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

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