Correction bug Notation: il faut re-déclarer les règles de parsing des notations au moment de la déclaration d'interprétation car la règle de parsing peut être dans un autre fichier qui n'est pas importé

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

2 files changed, 17 insertions, 7 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index b842c45df..d73e80f74 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -20,10 +20,11 @@ open Nameops
 
 (* State of the grammar extensions *)
 
+type notation_grammar = 
+    int * Gramext.g_assoc option * notation * prod_item list * int list option
+
 type all_grammar_command =
-  | Notation of
-      (int * Gramext.g_assoc option * notation * prod_item list *
-      int list option)
+  | Notation of Symbols.level * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
@@ -415,7 +416,7 @@ let add_tactic_entries gl =
 
 let extend_grammar gram =
   (match gram with
-  | Notation a -> extend_constr_notation a
+  | Notation (_,a) -> extend_constr_notation a
   | Grammar g -> extend_grammar_rules g
   | TacticGrammar l -> add_tactic_entries l);
   grammar_state := gram :: !grammar_state
@@ -428,6 +429,12 @@ let reset_extend_grammars_v8 () =
   List.iter (fun (s,gl) -> extend_tactic_grammar s gl) te;
   List.iter (fun (s,gl) -> extend_vernac_command_grammar s gl) tv
 
+let recover_notation_grammar ntn prec =
+  let l = map_succeed (function
+    | Notation (prec',(_,_,ntn',_,_ as x)) when prec = prec' & ntn = ntn' -> x
+    | _ -> failwith "") !grammar_state in
+  assert (List.length l = 1);
+  List.hd l
 
 (* Summary functions: the state of the lexer is included in that of the parser.
    Because the grammar affects the set of keywords when adding or removing
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index b6844e547..f54b31484 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -19,10 +19,11 @@ open Rawterm
 open Mod_subst
 (*i*)
 
+type notation_grammar = 
+    int * Gramext.g_assoc option * notation * prod_item list * int list option
+
 type all_grammar_command =
-  | Notation of
-      (int * Gramext.g_assoc option * notation * prod_item list *
-      int list option)
+  | Notation of Symbols.level * notation_grammar
   | Grammar of grammar_command
   | TacticGrammar of
       (string * (string * grammar_production list) * 
@@ -53,3 +54,5 @@ val subst_all_grammar_command :
 
 val interp_entry_name : string -> string -> 
   entry_type * Token.t Gramext.g_symbol
+
+val recover_notation_grammar :  notation -> Symbols.level -> notation_grammar