From 15bcd883c3266050ec3a3389c19712ad5df2d6c5 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Tue, 31 Aug 2010 13:59:42 +0000
Subject: * By default, load proof terms.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13389 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/flags.ml      | 2 +-
 toplevel/usage.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/flags.ml b/lib/flags.ml
index 1cb79cb7ab..cb450a5dba 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -29,7 +29,7 @@ let term_quality = ref false
 
 let xml_export = ref false
 
-let load_proofs = ref false
+let load_proofs = ref true
 
 let raw_print = ref false
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 9a6cd095e0..a3dbff23c1 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -61,8 +61,8 @@ let print_usage_channel co command =
   -dump-glob f           dump globalizations in file f (to be used by coqdoc)
   -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
   -impredicative-set     set sort Set impredicative
-  -dont-load-proofs      don't load opaque proofs in memory (default)
-  -load-proofs           load opaque proofs in memory
+  -load-proofs           load opaque proofs in memory (default)
+  -dont-load-proofs      don't load opaque proofs in memory 
   -xml                   export XML files either to the hierarchy rooted in
                          the directory $COQ_XML_LIBRARY_ROOT (if set) or to
                          stdout (if unset)
-- 
cgit v1.2.3