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, 27 insertions, 27 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ec74c91b25..1117d25079 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -67,12 +67,12 @@ let print_projections = ref false
 
 let print_meta_as_hole = ref false
 
-let with_arguments f = Options.with_option print_arguments f
-let with_implicits f = Options.with_option print_implicits f
-let with_coercions f = Options.with_option print_coercions f
-let with_universes f = Options.with_option print_universes f
-let without_symbols f = Options.with_option print_no_symbol f
-let with_meta_as_hole f = Options.with_option print_meta_as_hole f
+let with_arguments f = Flags.with_option print_arguments f
+let with_implicits f = Flags.with_option print_implicits f
+let with_coercions f = Flags.with_option print_coercions f
+let with_universes f = Flags.with_option print_universes f
+let without_symbols f = Flags.with_option print_no_symbol f
+let with_meta_as_hole f = Flags.with_option print_meta_as_hole f
 
 (**********************************************************************)
 (* Various externalisation functions *)
@@ -409,7 +409,7 @@ let match_aconstr_cases_pattern c (metas_scl,pat) =
  (* Better to use extern_rawconstr composed with injection/retraction ?? *)
 let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     let (na,sc,p) = uninterp_prim_token_cases_pattern pat in
     match availability_of_prim_token sc scopes with
     | None -> raise No_match
@@ -418,7 +418,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
       insert_pat_alias loc (insert_pat_delimiters loc (CPatPrim(loc,p)) key) na
   with No_match ->
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     extern_symbol_pattern scopes vars pat
       (uninterp_cases_pattern_notations pat)
   with No_match ->
@@ -451,7 +451,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes' = option_cons scopt scopes in
+	          let scopes' = Option.List.cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern_cases_pattern_in_scope (scopt,scl@scopes') vars c)
@@ -476,7 +476,7 @@ let occur_name na aty =
     | Anonymous -> false
 
 let is_projection nargs = function
-  | Some r when not !Options.raw_print & !print_projections ->
+  | Some r when not !Flags.raw_print & !print_projections ->
       (try 
 	let n = Recordops.find_projection_nparams r + 1 in
 	if n <= nargs then Some n else None
@@ -496,7 +496,7 @@ let explicitize loc inctx impl (cf,f) args =
     | a::args, imp::impl when is_status_implicit imp ->
         let tail = exprec (q+1) (args,impl) in
         let visible =
-          !Options.raw_print or
+          !Flags.raw_print or
           (!print_implicits & !print_implicits_explicit_args) or 
 	  (!print_implicits_defensive &
 	   is_significant_implicit a impl tail &
@@ -535,7 +535,7 @@ let extern_app loc inctx impl (cf,f) args =
     extern_global loc impl f
   else
   if 
-    ((!Options.raw_print or
+    ((!Flags.raw_print or
       (!print_implicits & not !print_implicits_explicit_args)) &
      List.exists is_status_implicit impl)
   then 
@@ -554,7 +554,7 @@ let rec extern_args extern scopes env args subscopes =
 
 let rec remove_coercions inctx = function
   | RApp (loc,RRef (_,r),args) as c
-      when  not (!Options.raw_print or !print_coercions)
+      when  not (!Flags.raw_print or !print_coercions)
       ->
       let nargs = List.length args in
       (try match Classops.hide_coercion r with
@@ -638,11 +638,11 @@ let extern_rawsort = function
 let rec extern inctx scopes vars r =
   let r' = remove_coercions inctx r in
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     extern_optimal_prim_token scopes r r'
   with No_match ->
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     extern_symbol scopes vars r' (uninterp_notations r')
   with No_match -> match r' with
   | RRef (loc,ref) ->
@@ -772,7 +772,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
 
 and factorize_prod scopes vars aty c =
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
   | RProd (loc,(Name id as na),ty,c)
@@ -784,7 +784,7 @@ and factorize_prod scopes vars aty c =
 
 and factorize_lambda inctx scopes vars aty c =
   try 
-    if !Options.raw_print or !print_no_symbol then raise No_match;
+    if !Flags.raw_print or !print_no_symbol then raise No_match;
     ([],extern_symbol scopes vars c (uninterp_notations c))
   with No_match -> match c with
   | RLambda (loc,na,ty,c)
@@ -845,7 +845,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
-	          let scopes' = option_cons scopt scopes in
+	          let scopes' = Option.List.cons scopt scopes in
 	          let l =
 		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6fc7a7d310..a418253462 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -10,7 +10,7 @@
 
 open Pp
 open Util
-open Options
+open Flags
 open Names
 open Nameops
 open Libnames
@@ -221,7 +221,7 @@ let contract_pat_notation ntn l =
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
-let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
+let make_current_scope (tmp_scope,scopes) = Option.List.cons tmp_scope scopes
 
 let set_var_scope loc id (_,scopt,scopes) varscopes =
   let idscopes = List.assoc id varscopes in
diff --git a/interp/notation.ml b/interp/notation.ml
index d5de23bc5d..b04f3be035 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -73,7 +73,7 @@ let init_scope_map () =
 let declare_scope scope =
   try let _ = Gmap.find scope !scope_map in ()
   with Not_found ->
-(*    Options.if_verbose message ("Creating scope "^scope);*)
+(*    Flags.if_verbose message ("Creating scope "^scope);*)
     scope_map := Gmap.add scope empty_scope !scope_map
 
 let find_scope scope =
@@ -142,16 +142,16 @@ let delimiters_map = ref Gmap.empty
 
 let declare_delimiters scope key =
   let sc = find_scope scope in
-  if sc.delimiters <> None && Options.is_verbose () then begin
+  if sc.delimiters <> None && Flags.is_verbose () then begin
     let old = Option.get sc.delimiters in
-    Options.if_verbose 
+    Flags.if_verbose 
       warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
   end;
   let sc = { sc with delimiters = Some key } in
   scope_map := Gmap.add scope sc !scope_map;
   if Gmap.mem key !delimiters_map then begin
     let oldsc = Gmap.find key !delimiters_map in
-    Options.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
+    Flags.if_verbose warning ("Hiding binding of key "^key^" to "^oldsc)
   end;
   delimiters_map := Gmap.add key scope !delimiters_map
 
@@ -300,7 +300,7 @@ let declare_notation_interpretation ntn scopt pat df =
   let scope = match scopt with Some s -> s | None -> default_scope in
   let sc = find_scope scope in
   if Gmap.mem ntn sc.notations then
-    Options.if_warn msg_warning (str ("Notation "^ntn^" was already used"^
+    Flags.if_warn msg_warning (str ("Notation "^ntn^" was already used"^
     (if scopt = None then "" else " in scope "^scope)));
   let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in
   scope_map := Gmap.add scope sc !scope_map;
@@ -637,7 +637,7 @@ let error_notation_not_reference loc ntn =
 let interp_notation_as_global_reference loc test ntn =
   let ntns = browse_notation true ntn !scope_map in
   let refs = List.map (global_reference_of_notation test) ntns in
-  match filter_some refs with
+  match Option.List.flatten refs with
   | [_,_,ref] -> ref
   | [] -> error_notation_not_reference loc ntn
   | refs -> 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 131ce29701..02e15f0690 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -85,7 +85,7 @@ let rec unloc = function
 let anonymize_if_reserved na t = match na with
   | Name id as na ->
       (try 
-	if not !Options.raw_print & unloc t = find_reserved_type id
+	if not !Flags.raw_print & unloc t = find_reserved_type id
 	then RHole (dummy_loc,Evd.BinderType na)
 	else t
       with Not_found -> t)