aboutsummaryrefslogtreecommitdiff
path: root/parsing/printer.ml
diff options
context:
space:
mode:
authoraspiwack2007-12-06 17:36:14 +0000
committeraspiwack2007-12-06 17:36:14 +0000
commita59b644de4234fb7fe3fce28284979091f257130 (patch)
treed5d8ff609aa9e4e582a06ca865a94eee1edbf182 /parsing/printer.ml
parent3e3fa18a066feae44c10fc6e072059f4e9914656 (diff)
Plus de combinateurs sont passés de Util à Option. Le module Options
devient Flags. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10348 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/printer.ml')
-rw-r--r--parsing/printer.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 52e5cb836c..ac21550983 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -30,7 +30,7 @@ open Ppconstr
open Constrextern
let emacs_str s alts =
- match !Options.print_emacs, !Options.print_emacs_safechar with
+ match !Flags.print_emacs, !Flags.print_emacs_safechar with
| true, true -> alts
| true , false -> s
| false,_ -> ""
@@ -227,7 +227,7 @@ let pr_context_limit n env =
in
(sign_env ++ db_env)
-let pr_context_of env = match Options.print_hyps_limit () with
+let pr_context_of env = match Flags.print_hyps_limit () with
| None -> hv 0 (pr_context_unlimited env)
| Some n -> hv 0 (pr_context_limit n env)