diff options
| author | Enrico Tassi | 2018-04-12 09:54:36 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-12 09:54:36 +0200 |
| commit | d54b8dff818f0b1218df14cfb2b813da93154fa9 (patch) | |
| tree | b89257dd429d6d57c7efbe6403b9a231392b2a8b /mathcomp/ssrtest/caseview.v | |
| parent | c17414bbef21bb3d0b96ee004c29ef7d56e55e2e (diff) | |
remove ssrtest: it now belongs to Coq
Diffstat (limited to 'mathcomp/ssrtest/caseview.v')
| -rw-r--r-- | mathcomp/ssrtest/caseview.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/mathcomp/ssrtest/caseview.v b/mathcomp/ssrtest/caseview.v deleted file mode 100644 index 478f573..0000000 --- a/mathcomp/ssrtest/caseview.v +++ /dev/null @@ -1,7 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. - - -Lemma test (A B : Prop) : A /\ B -> True. -Proof. by case=> _ /id _. Qed.
\ No newline at end of file |