diff options
Diffstat (limited to 'mathcomp/ssrtest/ssrsyntax2.v')
| -rw-r--r-- | mathcomp/ssrtest/ssrsyntax2.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/mathcomp/ssrtest/ssrsyntax2.v b/mathcomp/ssrtest/ssrsyntax2.v deleted file mode 100644 index 5e174a2..0000000 --- a/mathcomp/ssrtest/ssrsyntax2.v +++ /dev/null @@ -1,11 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssrtest.ssrsyntax1. -Require Import Arith. - -Goal (forall a b, a + b = b + a). -intros. -rewrite plus_comm, plus_comm. -split. -Qed. - |