From d14635b0c74012e464aad9e77aeeffda0f1ef154 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 8 Jun 2010 13:56:14 +0000
Subject: Made option "Automatic Introduction" active by default before too
 many people use the undocumented "Lemma foo x : t" feature in a way
 incompatible with this activation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/flags.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/flags.ml b/lib/flags.ml
index cb87e2f2b6..28d8cd07b6 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -61,7 +61,7 @@ let verbosely f x = without_option silent f x
 let if_silent f x = if !silent then f x
 let if_verbose f x = if not !silent then f x
 
-let auto_intros = ref false
+let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
 let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
 
-- 
cgit v1.2.3