From 77d86619f5f557de52a391f6811bacd73c01580b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Dec 2009 21:22:21 +0000
Subject: Renouncing to have the option "Automatic Introduction" on by default.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12613 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Fixpoint.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index fcf8d8d4a7..3a4f88993f 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -50,6 +50,8 @@ End folding.
 
 (* Check definition by tactics *)
 
+Set Automatic Introduction.
+
 Inductive even : nat -> Type :=
   | even_O : even 0
   | even_S : forall n, odd n -> even (S n)
-- 
cgit v1.2.3