Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de printers dans ocamldebug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6546 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 16 insertions, 16 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 3acf6904b2..4b7659cafd 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -24,7 +24,7 @@ type notation_grammar =
     int * Gramext.g_assoc option * notation * prod_item list * int list option
 
 type all_grammar_command =
-  | Notation of Symbols.level * notation_grammar
+  | Notation of Notation.level * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 464c1fffd9..1ee900dbcd 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -19,7 +19,7 @@ open Ppextend
 open Names
 open Nametab
 open Topconstr
-open Symbols
+open Notation
  
 (*** Syntax keys ***)
 
@@ -228,7 +228,7 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
 	  (* Test for a primitive printer; may raise Not_found *)
 	  let sc,pr = lookup_primitive_printer c in
 	  (* Look if scope [sc] associated to this printer is OK *)
-	  (match Symbols.availability_of_numeral sc scopes with
+	  (match Notation.availability_of_numeral sc scopes with
 	    | None -> otherwise ()
 	    | Some key ->
 	        (* We can use this printer *)
@@ -237,12 +237,12 @@ let call_primitive_parser rec_pr otherwise inherited scopes (se,env) =
 		  | Some strm -> print_delimiters inherited se strm key
 		  | None -> otherwise ())
     | [UNP_SYMBOLIC (sc,pat,sub)] ->
-	(match Symbols.availability_of_notation (sc,pat) scopes with
+	(match Notation.availability_of_notation (sc,pat) scopes with
 	  | None -> otherwise ()
 	  | Some (scopt,key) ->
 	      print_delimiters inherited se
 		(print_syntax_entry rec_pr
-		  (option_fold_right Symbols.push_scope scopt scopes) env 
+		  (option_fold_right Notation.push_scope scopt scopes) env 
 		  {se with syn_hunks = [sub]}) key)
     | _ ->
 	pr_parenthesis inherited se (print_syntax_entry rec_pr scopes env se)
@@ -270,7 +270,7 @@ let genprint dflt whatfor inhprec ast =
     in test_rule entries
   in
   try 
-    rec_pr (Symbols.current_scopes ()) inhprec ast
+    rec_pr (Notation.current_scopes ()) inhprec ast
   with
     | Failure _ -> (str"<PP failure: " ++ dflt ast ++ str">")
     | Not_found -> (str"<PP search failure: " ++ dflt ast ++ str">")
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index 6d61d01221..d6a7f44689 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -11,7 +11,7 @@
 (*i*)
 open Pp
 open Extend
-open Symbols
+open Notation
 open Ppextend
 open Topconstr
 (*i*)
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index 8fe0536eb6..85b79d8bf5 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -111,7 +111,7 @@ open Rawterm
 open Libnames
 open Bigint
 open Coqlib
-open Symbols
+open Notation
 open Pp
 open Util
 open Names
@@ -187,7 +187,7 @@ let uninterp_nat_pattern p =
 (* Declare the primitive parsers and printers *)
 
 let _ =
-  Symbols.declare_numeral_interpreter "nat_scope"
+  Notation.declare_numeral_interpreter "nat_scope"
     (glob_nat,["Coq";"Init";"Datatypes"])
     (nat_of_int,Some pat_nat_of_int)
     ([RRef (dummy_loc,glob_S); RRef (dummy_loc,glob_O)], uninterp_nat, None)
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml
index ef6fdeb7e7..3cd6eba3a2 100644
--- a/parsing/g_rsyntax.ml
+++ b/parsing/g_rsyntax.ml
@@ -278,7 +278,7 @@ let uninterp_r p =
   with Non_closed_number ->
     None
 
-let _ = Symbols.declare_numeral_interpreter "R_scope"
+let _ = Notation.declare_numeral_interpreter "R_scope"
   (glob_R,["Coq";"Reals";"Rdefinitions"])
   ((if !Options.v7 then r_of_int2 else r_of_int),None)
   ([RRef(dummy_loc,glob_Ropp);RRef(dummy_loc,glob_R0);
diff --git a/parsing/g_zsyntax.ml b/parsing/g_zsyntax.ml
index e6cbda7124..cae9c76f2d 100644
--- a/parsing/g_zsyntax.ml
+++ b/parsing/g_zsyntax.ml
@@ -223,7 +223,7 @@ let uninterp_positive p =
 (* Declaring interpreters and uninterpreters for positive *)
 (************************************************************************)
 
-let _ = Symbols.declare_numeral_interpreter "positive_scope"
+let _ = Notation.declare_numeral_interpreter "positive_scope"
   (glob_positive,positive_module)
   (interp_positive,Some pat_interp_positive)
   ([RRef (dummy_loc, glob_xI); 
@@ -284,7 +284,7 @@ let uninterp_n p =
 (************************************************************************)
 (* Declaring interpreters and uninterpreters for N *)
 
-let _ = Symbols.declare_numeral_interpreter "N_scope"
+let _ = Notation.declare_numeral_interpreter "N_scope"
   (glob_n,binnat_module)
   (n_of_int,Some pat_n_of_int)
   ([RRef (dummy_loc, glob_N0); 
@@ -340,7 +340,7 @@ let uninterp_z p =
 (************************************************************************)
 (* Declaring interpreters and uninterpreters for Z *)
 
-let _ = Symbols.declare_numeral_interpreter "Z_scope"
+let _ = Notation.declare_numeral_interpreter "Z_scope"
   (glob_z,fast_integer_module)
   (z_of_int,Some pat_z_of_int)
   ([RRef (dummy_loc, glob_ZERO); 
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index c3d865c0e4..37abe40633 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -54,7 +54,7 @@ let decode_patlist_value = function
   | CPatCstr (_,_,l) -> l
   | _ -> anomaly "Ill-formed list argument of notation"
 
-open Symbols
+open Notation
 
 let rec print_hunk n decode pr env = function
   | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index da915f17bb..743036bcf5 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -113,7 +113,7 @@ let print_opacity ref =
     
 let print_name_infos ref =
   let impl = implicits_of_global ref in
-  let scopes = Symbols.find_arguments_scope ref in
+  let scopes = Notation.find_arguments_scope ref in
   let type_for_implicit = 
     if need_expansion impl ref then
       (* Need to reduce since implicits are computed with products flattened *)
@@ -149,7 +149,7 @@ let print_inductive_implicit_args =
 
 let print_inductive_argument_scopes =
   print_args_data_of_inductive_ids 
-    Symbols.find_arguments_scope ((<>) None) print_argument_scopes
+    Notation.find_arguments_scope ((<>) None) print_argument_scopes
 
 (*********************)
 (* "Locate" commands *)