From d54b8dff818f0b1218df14cfb2b813da93154fa9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 12 Apr 2018 09:54:36 +0200
Subject: remove ssrtest: it now belongs to Coq

---
 mathcomp/ssrtest/testmx.v | 37 -------------------------------------
 1 file changed, 37 deletions(-)
 delete mode 100644 mathcomp/ssrtest/testmx.v

(limited to 'mathcomp/ssrtest/testmx.v')

diff --git a/mathcomp/ssrtest/testmx.v b/mathcomp/ssrtest/testmx.v
deleted file mode 100644
index 7d90d29..0000000
--- a/mathcomp/ssrtest/testmx.v
+++ /dev/null
@@ -1,37 +0,0 @@
-(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
-(* Distributed under the terms of CeCILL-B.                                  *)
-Require Import mathcomp.ssreflect.ssreflect.
-From mathcomp
-Require Import ssrfun ssrbool eqtype ssrnat.
-From mathcomp
-Require Import ssralg matrix.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Import Prenex Implicits.
-
-Local Open Scope nat_scope.
-Local Open Scope ring_scope.
-
-Section TestMx.
-
-Variable R : ringType.
-Variable M : 'M[R]_2.
-
-Goal 1%:M = M.
-Proof.
-Set Printing All.
-rewrite [(1%:M : 'M_(1+1)%N)]scalar_mx_block.
-(* Success with 1.2 *)
-(* With ssreflect 1.3, fails with error : *)
-(* Toplevel input, characters 0-44: *)
-(* Error: pattern (1%:M) does not match LHS of scalar_mx_block *)
-Admitted.
-
-Goal 1%:M = M.
-Proof.
-rewrite [1%:M](scalar_mx_block 1%N 1%N).
-(* Success in both ssr 1.2 and 1.3 *)
-Admitted.
-
-End TestMx.
\ No newline at end of file
-- 
cgit v1.2.3