Moving notation types into grammar rule.

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

2 files changed, 12 insertions, 16 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index fcb4e7d7e..34e0dcdef 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -204,7 +204,8 @@ type notation_grammar = {
   notgram_level : int;
   notgram_assoc : gram_assoc option;
   notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list
+  notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : notation_var_internalization_type list;
 }
 
 let extend_constr_constr_notation ng =
@@ -252,10 +253,7 @@ type tactic_grammar = {
 }
 
 type all_grammar_command =
-  | Notation of
-	 (precedence * tolerability list) *
-	  notation_var_internalization_type list *
-	  notation_grammar
+  | Notation of Notation.level * notation_grammar
   | TacticGrammar of tactic_grammar
 
 (* Declaration of the tactic grammar rule *)
@@ -286,21 +284,21 @@ let (grammar_state : (int * all_grammar_command) list ref) = ref []
 
 let extend_grammar gram =
   let nb = match gram with
-  | Notation (_,_,a) -> extend_constr_notation a
+  | Notation (_,a) -> extend_constr_notation a
   | TacticGrammar g -> add_tactic_entry g in
   grammar_state := (nb,gram) :: !grammar_state
 
-let extend_constr_grammar pr typs ntn =
-  extend_grammar (Notation (pr, typs, ntn))
+let extend_constr_grammar pr ntn =
+  extend_grammar (Notation (pr, ntn))
 
 let extend_tactic_grammar ntn =
   extend_grammar (TacticGrammar ntn)
 
 let recover_constr_grammar ntn prec =
   let filter = function
-  | _, Notation (prec', vars, ng) when
+  | _, Notation (prec', ng) when
       Notation.level_eq prec prec' &&
-      String.equal ntn ng.notgram_notation -> Some (vars, ng)
+      String.equal ntn ng.notgram_notation -> Some ng
   | _ -> None
   in
   match List.map_filter filter !grammar_state with
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index dfae42ae4..9ae49f718 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -36,7 +36,8 @@ type notation_grammar = {
   notgram_level : int;
   notgram_assoc : gram_assoc option;
   notgram_notation : notation;
-  notgram_prods : grammar_constr_prod_item list list
+  notgram_prods : grammar_constr_prod_item list list;
+  notgram_typs : notation_var_internalization_type list;
 }
 
 type tactic_grammar = {
@@ -48,16 +49,13 @@ type tactic_grammar = {
 
 (** {5 Adding notations} *)
 
-val extend_constr_grammar :
-  Notation.level -> notation_var_internalization_type list ->
-  notation_grammar -> unit
+val extend_constr_grammar : Notation.level -> notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
 val extend_tactic_grammar : tactic_grammar -> unit
 (** Add a tactic notation rule to the parsing system. *)
 
-val recover_constr_grammar : notation -> Notation.level ->
-  notation_var_internalization_type list * notation_grammar
+val recover_constr_grammar : notation -> Notation.level -> notation_grammar
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)