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

4 files changed, 7 insertions, 7 deletions

diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 7cb4ad332d..b2c94cd6f9 100644
--- a/contrib/correctness/penv.ml
+++ b/contrib/correctness/penv.ml
@@ -233,7 +233,7 @@ let register id id' =
   try
     let (v,p) = Idmap.find id !edited in
     let _ = add_global id' v (Some p) in
-    Options.if_verbose 
+    Flags.if_verbose 
       msgnl (hov 0 (str"Program " ++ pr_id id' ++ spc () ++ str"is defined"));
     edited := Idmap.remove id !edited
   with Not_found -> ()
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index 23c1028a41..aaa304fe53 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -21,12 +21,12 @@ open Topconstr
 (* debug *)
 
 let deb_mess s =
-  if !Options.debug then begin
+  if !Flags.debug then begin
     msgnl s; pp_flush()
   end
 
 let deb_print f x =
-  if !Options.debug then begin
+  if !Flags.debug then begin
     msgnl (f x); pp_flush()
   end
 
@@ -49,7 +49,7 @@ let reraise_with_loc loc f x =
 
 (* functions on names *)
 
-let at = if !Options.v7 then "@" else "'at'"
+let at = if !Flags.v7 then "@" else "'at'"
 
 let at_id id d = id_of_string ((string_of_id id) ^ at ^ d)
 
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index bb9a355c3f..df1b67fd3f 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -13,7 +13,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-open Options
+open Flags
 open Util
 open Names
 open Nameops
@@ -228,7 +228,7 @@ let mk_prog loc p pre post =
     loc = loc; 
     info = () }
 
-if !Options.v7 then
+if !Flags.v7 then
 GEXTEND Gram
 
   (* Types ******************************************************************)
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index b99a3621d8..76ba04c514 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -11,7 +11,7 @@
 (* $Id$ *)
 
 open Pp
-open Options
+open Flags
 open Names
 open Libnames
 open Term