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

8 files changed, 19 insertions, 19 deletions

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 8b8761cb18..c62c813778 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -33,7 +33,7 @@ open Names
 let nat_of_int dloc n =
   if is_pos_or_zero n then begin
       if less_than (of_string "5000") n then
-	Options.if_warn msg_warning 
+	Flags.if_warn msg_warning 
 	  (strbrk "Stack overflow or segmentation fault happens when " ++
 	   strbrk "working with large numbers in nat (observed threshold " ++
 	   strbrk "may vary from 5000 to 70000 depending on your system " ++
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a7a78f7700..729693aa7d 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -105,7 +105,7 @@ END
 
 let test_plurial_form = function
   | [(_,([_],_))] ->
-      Options.if_verbose warning
+      Flags.if_verbose warning
    "Keywords Variables/Hypotheses/Parameters expect more than one assumption"
   | _ -> ()
 
@@ -143,7 +143,7 @@ GEXTEND Gram
       | IDENT "Unboxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,false)
        | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (recs,Options.boxed_definitions())
+          VernacFixpoint (recs,Flags.boxed_definitions())
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
           VernacCoFixpoint (corecs,false)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
@@ -175,11 +175,11 @@ GEXTEND Gram
   ;
   def_token:
     [ [ "Definition" -> 
-	no_hook, (Global, Options.boxed_definitions(), Definition)
+	no_hook, (Global, Flags.boxed_definitions(), Definition)
       | IDENT "Let" -> 
-	no_hook, (Local, Options.boxed_definitions(), Definition)
+	no_hook, (Local, Flags.boxed_definitions(), Definition)
       | IDENT "Example" -> 
-	no_hook, (Global, Options.boxed_definitions(), Example)
+	no_hook, (Global, Flags.boxed_definitions(), Example)
       | IDENT "SubClass"  -> Class.add_subclass_hook, (Global, false, SubClass)
       | IDENT "Local"; IDENT "SubClass"  ->
           Class.add_subclass_hook, (Local, false, SubClass) ] ] 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index cfa62fa5ad..a711bb85a9 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -374,10 +374,10 @@ let null_comment s =
 
 let comment_stop ep =
   let current_s = Buffer.contents current in
-  if !Options.xml_export && Buffer.length current > 0 &&
+  if !Flags.xml_export && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
       !xml_output_comment current_s;
-  (if Options.do_translate() && Buffer.length current > 0 &&
+  (if Flags.do_translate() && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
     let bp = match !comment_begin with
         Some bp -> bp
@@ -412,7 +412,7 @@ let rec comment bp = parser bp2
          | [< '')' >] -> push_string "*)";
          | [< s >] -> real_push_char '*'; comment bp s >] -> ()
   | [< ''"'; s >] ->
-      if Options.do_translate() then (push_string"\"";comm_string bp2 s)
+      if Flags.do_translate() then (push_string"\"";comm_string bp2 s)
       else ignore (string bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
@@ -485,7 +485,7 @@ let rec next_token = parser bp
       (("METAIDENT", get_buff len), (bp,ep))
   | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
-      if Options.do_translate() & t=("",".") then between_com := true;
+      if Flags.do_translate() & t=("",".") then between_com := true;
       (t, (bp,ep))
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c);
        len = ident_tail (store 0 c) >] ep ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 07055869af..d2380dad6d 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -162,7 +162,7 @@ let camlp4_verbosity silent f x =
 
 let grammar_extend te pos rls =
   camlp4_state := ByGrammar (Gramobj.weaken_entry te,pos,rls) :: !camlp4_state;
-  camlp4_verbosity (Options.is_verbose ()) (G.extend te pos) rls
+  camlp4_verbosity (Flags.is_verbose ()) (G.extend te pos) rls
 
 (* n is the number of extended entries (not the number of Grammar commands!)
    to remove. *)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 8e542ce147..858c6685fd 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -96,13 +96,13 @@ let pr_delimiters key strm =
   strm ++ str ("%"^key)
 
 let pr_located pr (loc,x) =
-  if Options.do_translate() && loc<>dummy_loc then
+  if Flags.do_translate() && loc<>dummy_loc then
     let (b,e) = unloc loc in
     comment b ++ pr x ++ comment e
   else pr x
 
 let pr_com_at n =
-  if Options.do_translate() && n <> 0 then comment n 
+  if Flags.do_translate() && n <> 0 then comment n 
   else mt()
 
 let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index bbb481f3e2..1161c3b61a 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -570,7 +570,7 @@ let rec pr_vernac = function
       let pr_onerec = function
         | (id,(n,ro),bl,type_,def),ntn ->
             let (bl',def,type_) =
-              if Options.do_translate() then extract_def_binders def type_
+              if Flags.do_translate() then extract_def_binders def type_
               else ([],def,type_) in
             let bl = bl @ bl' in
             let ids = List.flatten (List.map name_of_binder bl) in
@@ -607,7 +607,7 @@ let rec pr_vernac = function
   | VernacCoFixpoint (corecs,b) ->
       let pr_onecorec ((id,bl,c,def),ntn) =
         let (bl',def,c) =
-              if Options.do_translate() then extract_def_binders def c
+              if Flags.do_translate() then extract_def_binders def c
               else ([],def,c) in
         let bl = bl @ bl' in
         pr_id id ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++
@@ -753,7 +753,7 @@ let rec pr_vernac = function
 	  (Global.env())
 	  body in
       hov 1
-        (((*if !Options.p1 then
+        (((*if !Flags.p1 then
 	  (if rc then str "Recursive " else mt()) ++
 	  str "Tactic Definition " else*)
 	    (* Rec by default *) str "Ltac ") ++
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index a3a0c2f152..9beba9347c 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -352,7 +352,7 @@ let gallina_print_inductive sp =
   let (mib,mip) = Global.lookup_inductive (sp,0) in
   let mipv = mib.mind_packets in
   let names = list_tabulate (fun x -> (sp,x)) (Array.length mipv) in
-  (if mib.mind_record & not !Options.raw_print then
+  (if mib.mind_record & not !Flags.raw_print then
     pr_record (List.hd names)
   else
     pr_mutual_inductive mib.mind_finite names) ++ fnl () ++
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)