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

20 files changed, 47 insertions, 47 deletions

diff --git a/contrib/correctness/penv.ml b/contrib/correctness/penv.ml
index 7cb4ad332..b2c94cd6f 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 23c1028a4..aaa304fe5 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 bb9a355c3..df1b67fd3 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 b99a3621d..76ba04c51 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
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 772a49742..abc7b1f04 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -305,7 +305,7 @@ let check_loaded_modfile mp = match base_mp mp with
   | _ -> ()
 
 let info_file f =   
-  Options.if_verbose message 
+  Flags.if_verbose message 
     ("The file "^f^" has been created by extraction.")
 
 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 45976d6e5..a10241a7c 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -47,7 +47,7 @@ let observe_tac_stream s tac g =
 let observe_tac s tac g = observe_tac_stream (str s) tac g
 
 (* let tclTRYD tac =  *)
-(*   if  !Options.debug  || do_observe () *)
+(*   if  !Flags.debug  || do_observe () *)
 (*   then (fun g -> try (\* do_observe_tac ""  *\)tac g with _ -> tclIDTAC g) *)
 (*   else tac *)
 
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index 72f930b0a..160764799 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -384,7 +384,7 @@ let generate_functional_principle
 	  { const_entry_body = value;
 	    const_entry_type = None;
 	    const_entry_opaque = false;
-	    const_entry_boxed = Options.boxed_definitions()
+	    const_entry_boxed = Flags.boxed_definitions()
 	  }
 	in
 	ignore(
@@ -394,7 +394,7 @@ let generate_functional_principle
 	     Decl_kinds.IsDefinition (Decl_kinds.Scheme)
 	    )
 	);
-	Options.if_verbose 
+	Flags.if_verbose 
 	  (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) 
 	  name;
 	names := name :: !names
@@ -655,7 +655,7 @@ let build_scheme fas =
 	 (Declare.declare_constant 
 	    princ_id 
 	    (Entries.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
-       Options.if_verbose 
+       Flags.if_verbose 
 	 (fun id -> Pp.msgnl (Ppconstr.pr_id id ++ str " is defined")) princ_id
     )
     fas
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 3102f1b5d..612be05e3 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -354,14 +354,14 @@ let register_struct is_rec fixpoint_exprl =
     | [(fname,_,bl,ret_type,body),_] when not is_rec -> 
 	Command.declare_definition
 	  fname
-	  (Decl_kinds.Global,Options.boxed_definitions (),Decl_kinds.Definition)
+	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
 	  bl
 	  None
   	  body
 	  (Some ret_type)
 	  (fun _ _ -> ())
     | _ -> 
-	Command.build_recursive fixpoint_exprl (Options.boxed_definitions())
+	Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref   
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
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
 
 
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index cf6246704..44df08598 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -819,7 +819,7 @@ let rec merge_mutual_inductive_body
 
   
 let rawterm_to_constr_expr x = (* build a constr_expr from a rawconstr *)
-  Options.with_option Options.raw_print (Constrextern.extern_rawtype Idset.empty) x
+  Flags.with_option Flags.raw_print (Constrextern.extern_rawtype Idset.empty) x
 
 let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = 
   let params = prms2 @ prms1 in
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index af0a2addc..2f6f5914d 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1181,8 +1181,8 @@ let do_build_inductive
     Array.map (List.map 
       (fun (id,t) -> 
 	 false,((dummy_loc,id),
-		Options.with_option
-		  Options.raw_print
+		Flags.with_option
+		  Flags.raw_print
 		  (Constrextern.extern_rawtype Idset.empty) ((* zeta_normalize *) t)
 	       )
       ))
@@ -1218,7 +1218,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in 
   try 
-    with_full_print (Options.silently (Command.build_mutual rel_inds)) true
+    with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
   with 
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/contrib/interface/centaur.ml4 b/contrib/interface/centaur.ml4
index 30c96f939..a2da3b07d 100644
--- a/contrib/interface/centaur.ml4
+++ b/contrib/interface/centaur.ml4
@@ -783,7 +783,7 @@ let start_pcoq_mode debug =
 *)
     set_pcoq_hook pcoq_hook;
     start_pcoq_objects();
-    Options.print_emacs := false; Pp.make_pp_nonemacs(); 
+    Flags.print_emacs := false; Pp.make_pp_nonemacs(); 
   end;;
 
 
diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index a948dd4d6..26b6b3094 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -109,7 +109,7 @@ let (teq_id:identifier) = hyp_id 15 hyp_ids;;
 let (pmax_id:identifier) = hyp_id 16 hyp_ids;;
 let (hle_id:identifier) = hyp_id 17 hyp_ids;;
 
-let message s = if Options.is_verbose () then msgnl(str s);;
+let message s = if Flags.is_verbose () then msgnl(str s);;
 
 let def_of_const t =
    match (kind_of_term t) with
@@ -948,7 +948,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n
 (*       (Array.make nb_goal ()) *)
 (*     ; *)
     ref := Some lemma ;
-    Options.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
+    Flags.silently Vernacentries.interp (Vernacexpr.VernacAbort None);
     build_proof 
       (  fun gls ->
 	   let hid = next_global_ident_away true h_id (pf_ids_of_hyps gls) in 
@@ -986,7 +986,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref goal_n
 	g);
   try
     by tclIDTAC; (* raises UserError _ if the proof is complete *)
-    if Options.is_verbose () then (pp (Printer.pr_open_subgoals()))
+    if Flags.is_verbose () then (pp (Printer.pr_open_subgoals()))
   with UserError _ -> 
     defined ()
   
@@ -1306,7 +1306,7 @@ let (com_eqn : identifier ->
        );
 (*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Options.silently (fun () ->Command.save_named opacity) () ;  
+     Flags.silently (fun () ->Command.save_named opacity) () ;  
 (*      Pp.msgnl (str "eqn finished"); *)
     
     );;
@@ -1377,7 +1377,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       and eq_ref = destConst (constr_of_global eq_ref) in
       generate_induction_principle f_ref tcc_lemma_constr
 	functional_ref eq_ref rec_arg_num rec_arg_type (nb_prod res) relation;
-      if Options.is_verbose ()
+      if Flags.is_verbose ()
       then msgnl (h 1 (Ppconstr.pr_id function_name ++ 
 			 spc () ++ str"is defined" )++ fnl () ++ 
 		    h 1 (Ppconstr.pr_id equation_id ++ 
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 97dd2f143..84568588c 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -12,7 +12,7 @@
 
 open Pp
 open Util
-open Options
+open Flags
 open Term
 open Names
 open Libnames
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 =