aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/funind/indfun_common.ml
diff options
context:
space:
mode:
authorGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 17:36:14 +0000
committerGravatar aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>2007-12-06 17:36:14 +0000
commita59b644de4234fb7fe3fce28284979091f257130 (patch)
treed5d8ff609aa9e4e582a06ca865a94eee1edbf182 /contrib/funind/indfun_common.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 'contrib/funind/indfun_common.ml')
-rw-r--r--contrib/funind/indfun_common.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index c2372d3ed..5ad4632e4 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -153,7 +153,7 @@ open Entries
open Decl_kinds
open Declare
let definition_message id =
- Options.if_verbose message ((string_of_id id) ^ " is defined")
+ Flags.if_verbose message ((string_of_id id) ^ " is defined")
let save with_clean id const (locality,kind) hook =
@@ -237,8 +237,8 @@ let with_full_print f a =
let old_implicit_args = Impargs.is_implicit_args ()
and old_strict_implicit_args = Impargs.is_strict_implicit_args ()
and old_contextual_implicit_args = Impargs.is_contextual_implicit_args () in
- let old_rawprint = !Options.raw_print in
- Options.raw_print := true;
+ let old_rawprint = !Flags.raw_print in
+ Flags.raw_print := true;
Impargs.make_implicit_args false;
Impargs.make_strict_implicit_args false;
Impargs.make_contextual_implicit_args false;
@@ -247,14 +247,14 @@ let with_full_print f a =
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
- Options.raw_print := old_rawprint;
+ Flags.raw_print := old_rawprint;
res
with
| e ->
Impargs.make_implicit_args old_implicit_args;
Impargs.make_strict_implicit_args old_strict_implicit_args;
Impargs.make_contextual_implicit_args old_contextual_implicit_args;
- Options.raw_print := old_rawprint;
+ Flags.raw_print := old_rawprint;
raise e