6 files changed, 17 insertions, 17 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index a3d95ab62..d1b4b50eb 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -14,7 +14,7 @@ open Util
 open Subtac_utils
 
 let trace s = 
-  if !Options.debug then (msgnl s; msgerr s)
+  if !Flags.debug then (msgnl s; msgerr s)
   else ()
 
 let succfix (depth, fixrels) = 
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 7fd08c7b0..c2691c781 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -17,7 +17,7 @@
 (* $Id$ *)
 
 
-open Options
+open Flags
 open Util
 open Names
 open Nameops
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 4617ca977..4f5e302c2 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -76,7 +76,7 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
       let _ = Typeops.infer_type env c in
 	Command.start_proof id kind c hook
       
-let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
+let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
 let start_proof_and_print env isevars idopt k t hook =
   start_proof_com env isevars idopt k t hook;
@@ -85,7 +85,7 @@ let start_proof_and_print env isevars idopt k t hook =
 let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n)))
   
 let assumption_message id =
-  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let declare_assumption env isevars idl is_coe k bl c nl =
   if not (Pfedit.refining ()) then 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 49eab5d29..a9a30c57a 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -349,7 +349,7 @@ let build_mutrec lnameargsardef boxed =
       ([],env,[],[]) lnameargsardef in
   let arityl = List.rev arityl in
   let notations = 
-    List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
+    List.fold_right (fun (_,ntnopt) l -> Option.List.cons ntnopt l) 
       lnameargsardef [] in
 
   let recdef =
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 5e7f025be..e3cf7a57a 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -43,7 +43,7 @@ type program_info = {
 }
 
 let assumption_message id =
-  Options.if_verbose message ((string_of_id id) ^ " is assumed")
+  Flags.if_verbose message ((string_of_id id) ^ " is assumed")
 
 let default_tactic : Proof_type.tactic ref = ref Refiner.tclIDTAC
 let default_tactic_expr : Tacexpr.glob_tactic_expr ref = ref (Obj.magic ())
@@ -248,11 +248,11 @@ type progress =
 let obligations_message rem =
   if rem > 0 then
     if rem = 1 then
-      Options.if_verbose msgnl (int rem ++ str " obligation remaining")
+      Flags.if_verbose msgnl (int rem ++ str " obligation remaining")
     else
-      Options.if_verbose msgnl (int rem ++ str " obligations remaining")
+      Flags.if_verbose msgnl (int rem ++ str " obligations remaining")
   else
-    Options.if_verbose msgnl (str "No more obligations remaining")
+    Flags.if_verbose msgnl (str "No more obligations remaining")
 
 let update_obls prg obls rem = 
   let prg' = { prg with prg_obligations = (obls, rem) } in
@@ -390,21 +390,21 @@ and try_solve_obligations n tac =
   try ignore (solve_obligations n tac) with NoObligations _ -> ()
 
 and auto_solve_obligations n : progress =
-  Options.if_verbose msgnl (str "Solving obligations automatically...");
+  Flags.if_verbose msgnl (str "Solving obligations automatically...");
   try solve_obligations n !default_tactic with NoObligations _ -> Dependent
       
 let add_definition n b t obls =
-  Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
+  Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked");
   let prg = init_prog_info n b t [] (Array.make 0 0) obls in
   let obls,_ = prg.prg_obligations in
   if Array.length obls = 0 then (
-    Options.if_verbose ppnl (str ".");    
+    Flags.if_verbose ppnl (str ".");    
     let cst = declare_definition prg in 
       from_prg := ProgMap.remove prg.prg_name !from_prg;
       Defined cst)
   else (
     let len = Array.length obls in
-    let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
+    let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in
       from_prg := ProgMap.add n prg !from_prg; 
       auto_solve_obligations (Some n))
 	
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 44638f496..d5df9adc9 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -113,20 +113,20 @@ let debug_on = true
 
 let debug n s = 
   if debug_on then
-    if !Options.debug && n >= debug_level then
+    if !Flags.debug && n >= debug_level then
       msgnl s
     else ()
   else ()
 
 let debug_msg n s = 
   if debug_on then
-    if !Options.debug  && n >= debug_level then s
+    if !Flags.debug  && n >= debug_level then s
     else mt ()
   else mt ()
 
 let trace s = 
   if debug_on then
-    if !Options.debug  && debug_level > 0 then msgnl s
+    if !Flags.debug  && debug_level > 0 then msgnl s
     else ()
   else ()
 
@@ -353,7 +353,7 @@ let recursive_message v =
 		    spc () ++ str "are recursively defined")
 
 let print_message m =
-  Options.if_verbose ppnl m
+  Flags.if_verbose ppnl m
 
 (* Solve an obligation using tactics, return the corresponding proof term *)
 let solve_by_tac evi t =