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

1 files changed, 6 insertions, 6 deletions

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 ->