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/elim_pattern.v | 19 -------------------
 1 file changed, 19 deletions(-)
 delete mode 100644 mathcomp/ssrtest/elim_pattern.v

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

diff --git a/mathcomp/ssrtest/elim_pattern.v b/mathcomp/ssrtest/elim_pattern.v
deleted file mode 100644
index 24bd0fb..0000000
--- a/mathcomp/ssrtest/elim_pattern.v
+++ /dev/null
@@ -1,19 +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 ssrbool eqtype ssrnat.
-Axiom daemon : False. Ltac myadmit := case: daemon.
-
-Lemma test x : (x == x) = (x + x.+1 == 2 * x + 1).
-case: (X in _ = X) / eqP => _.
-match goal with |- (x == x) = true => myadmit end.
-match goal with |- (x == x) = false => myadmit end.
-Qed.
-
-Lemma test1 x : (x == x) = (x + x.+1 == 2 * x + 1).
-elim: (x in RHS).
-match goal with |- (x == x) = _ => myadmit end.
-match goal with |- forall n, (x == x) = _ -> (x == x) = _ => myadmit end.
-Qed.
-
-- 
cgit v1.2.3