From fafd4dac5315e1d4e071b0044a50a16360b31964 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Thu, 23 Nov 2017 16:33:36 +0100
Subject: running semi-automated linting on the whole library

---
 mathcomp/attic/tutorial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/attic/tutorial.v')

diff --git a/mathcomp/attic/tutorial.v b/mathcomp/attic/tutorial.v
index 332d841..b2025a7 100644
--- a/mathcomp/attic/tutorial.v
+++ b/mathcomp/attic/tutorial.v
@@ -59,7 +59,7 @@ Lemma andb_sym2 : forall A B : bool, A && B -> B && A.
 Proof. by case; case. Qed.
 
 Lemma andb_sym3 : forall A B : bool, A && B -> B && A.
-Proof. by do 2! case. Qed.
+Proof. by do 2!case. Qed.
 
 Variables (C D : Prop) (hC : C) (hD : D).
 Check (and C D).
-- 
cgit v1.2.3