Merge remote-tracking branch 'github/pr/194' into trunk

2 files changed, 19 insertions, 14 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index b19fd9e1f..7ad104d03 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -967,23 +967,27 @@ let pr_visibility prglob = function
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
 (* Concrete syntax for symbolic-extension table *)
-let printing_rules =
-  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules) String.Map.t)
+let notation_rules =
+  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
 
-let declare_notation_printing_rule ntn ~extra unpl =
-  printing_rules := String.Map.add ntn (unpl,extra) !printing_rules
+let declare_notation_rule ntn ~extra unpl gram =
+  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
 
 let find_notation_printing_rule ntn =
-  try fst (String.Map.find ntn !printing_rules)
+  try pi1 (String.Map.find ntn !notation_rules)
   with Not_found -> anomaly (str "No printing rule found for " ++ str ntn)
 let find_notation_extra_printing_rules ntn =
-  try snd (String.Map.find ntn !printing_rules)
+  try pi2 (String.Map.find ntn !notation_rules)
   with Not_found -> []
+let find_notation_parsing_rules ntn =
+  try pi3 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn)
+
 let add_notation_extra_printing_rule ntn k v =
   try
-    printing_rules := 
-      let p, pp = String.Map.find ntn !printing_rules in
-      String.Map.add ntn (p, (k,v) :: pp) !printing_rules
+    notation_rules :=
+      let p, pp, gr = String.Map.find ntn !notation_rules in
+      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
   with Not_found ->
     user_err_loc (Loc.ghost,"add_notation_extra_printing_rule",
       str "No such Notation.")
@@ -993,7 +997,7 @@ let add_notation_extra_printing_rule ntn k v =
 
 let freeze _ =
  (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
-  !delimiters_map, !notations_key_table, !printing_rules,
+  !delimiters_map, !notations_key_table, !notation_rules,
   !scope_class_map)
 
 let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
@@ -1003,7 +1007,7 @@ let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
-  printing_rules := pprules;
+  notation_rules := pprules;
   scope_class_map := clsc
 
 let init () =
@@ -1011,7 +1015,7 @@ let init () =
   notation_level_map := String.Map.empty;
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
-  printing_rules := String.Map.empty;
+  notation_rules := String.Map.empty;
   scope_class_map := initial_scope_class_map
 
 let _ =
diff --git a/interp/notation.mli b/interp/notation.mli
index 480979ccc..a85dc50f2 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -196,10 +196,11 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-val declare_notation_printing_rule :
-  notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_notation_rule :
+  notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
 val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
 (** Rem: printing rules for primitive token are canonical *)