aboutsummaryrefslogtreecommitdiff
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/flags.ml2
-rw-r--r--lib/flags.mli2
2 files changed, 2 insertions, 2 deletions
diff --git a/lib/flags.ml b/lib/flags.ml
index 1b92aaf339..1cb79cb7ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -29,7 +29,7 @@ let term_quality = ref false
let xml_export = ref false
-let dont_load_proofs = ref false
+let load_proofs = ref false
let raw_print = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 1d18b4c516..7c46686778 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,7 +21,7 @@ val term_quality : bool ref
val xml_export : bool ref
-val dont_load_proofs : bool ref
+val load_proofs : bool ref
val raw_print : bool ref