Moving notation types into grammar rule.

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

3 files changed, 20 insertions, 26 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index fcb4e7d7e1..34e0dcdef2 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 dfae42ae4c..9ae49f718a 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) *)
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c8982692b1..4bce9b73e8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -750,7 +750,6 @@ let error_incompatible_level ntn oldprec prec =
     pr_level ntn prec ++ str ".")
 
 type syntax_extension = {
-  synext_intern : notation_var_internalization_type list;
   synext_level : Notation.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
@@ -769,7 +768,7 @@ let cache_one_syntax_extension se =
     (* Reserve the notation level *)
     Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
-    Egramcoq.extend_constr_grammar prec se.synext_intern se.synext_notgram;
+    Egramcoq.extend_constr_grammar prec se.synext_notgram;
     (* Declare the printing rule *)
     Notation.declare_notation_printing_rule ntn (se.synext_unparsing, fst prec)
 
@@ -1111,9 +1110,8 @@ let recover_syntax ntn =
   try
     let prec = Notation.level_of_notation ntn in
     let pp_rule,_ = Notation.find_notation_printing_rule ntn in
-    let typs, pa_rule = Egramcoq.recover_constr_grammar ntn prec in
-    { synext_intern = typs;
-      synext_level = prec;
+    let pa_rule = Egramcoq.recover_constr_grammar ntn prec in
+    { synext_level = prec;
       synext_notation = ntn;
       synext_notgram = pa_rule;
       synext_unparsing = pp_rule; }
@@ -1129,18 +1127,19 @@ let recover_notation_syntax rawntn =
   let sy = recover_syntax ntn in
   let need_squash = not (String.equal ntn rawntn) in
   let rules = if need_squash then recover_squash_syntax sy else [sy] in
-  sy.synext_intern, rules
+  sy.synext_notgram.notgram_typs, rules
 
 (**********************************************************************)
 (* Main entry point for building parsing and printing rules           *)
 
-let make_pa_rule (n,typs,symbols,_) ntn =
+let make_pa_rule i_typs (n,typs,symbols,_) ntn =
   let assoc = recompute_assoc typs in
   let prod = make_production typs symbols in
   { notgram_level = n;
     notgram_assoc = assoc;
     notgram_notation = ntn;
-    notgram_prods = prod; }
+    notgram_prods = prod;
+    notgram_typs = i_typs; }
 
 let make_pp_rule (n,typs,symbols,fmt) =
   match fmt with
@@ -1148,10 +1147,9 @@ let make_pp_rule (n,typs,symbols,fmt) =
   | Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
 
 let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) =
-  let pa_rule = make_pa_rule sy_data ntn in
+  let pa_rule = make_pa_rule i_typs sy_data ntn in
   let pp_rule = make_pp_rule sy_data in
   let sy = {
-    synext_intern = i_typs;
     synext_level = prec;
     synext_notation = ntn;
     synext_notgram = pa_rule;