From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Wed, 21 Jul 2010 09:46:51 +0200
Subject: Imported Upstream snapshot 8.3~beta0+13298

---
 test-suite/bugs/closed/shouldsucceed/2001.v | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'test-suite/bugs/closed/shouldsucceed/2001.v')

diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
index 323021de..d0b3bf17 100644
--- a/test-suite/bugs/closed/shouldsucceed/2001.v
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -1,8 +1,10 @@
 (* Automatic computing of guard in "Theorem with"; check that guard is not
    computed when the user explicitly indicated it *)
 
+Unset Automatic Introduction.
+
 Inductive T : Set :=
-| v : T. 
+| v : T.
 
 Definition f (s:nat) (t:T) : nat.
 fix 2.
@@ -12,9 +14,9 @@ refine
   | v => s
   end.
 Defined.
-           
+
 Lemma test :
   forall s, f s v = s.
-Proof.    
+Proof.
 reflexivity.
-Qed.        
+Qed.
-- 
cgit v1.2.3