Cleaning and documenting Egramcoq.

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

3 files changed, 20 insertions, 18 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 2e83c2b6b9..fcb4e7d7e1 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -290,7 +290,13 @@ let extend_grammar gram =
   | TacticGrammar g -> add_tactic_entry g in
   grammar_state := (nb,gram) :: !grammar_state
 
-let recover_notation_grammar ntn prec =
+let extend_constr_grammar pr typs ntn =
+  extend_grammar (Notation (pr, typs, 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.level_eq prec prec' &&
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 7cf3bab69a..dfae42ae4c 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -46,28 +46,24 @@ type tactic_grammar = {
   tacgram_tactic : DirPath.t * Tacexpr.glob_tactic_expr;
 }
 
-(** Adding notations *)
+(** {5 Adding notations} *)
 
-type all_grammar_command =
-  | Notation of
-	 (precedence * tolerability list)
-	  * notation_var_internalization_type list
-	   (** not needed for defining grammar, hosted by egrammar for
-	       transmission to interp_aconstr (via recover_notation_grammar) *)
-	  * notation_grammar
-  | TacticGrammar of tactic_grammar
+val extend_constr_grammar :
+  Notation.level -> notation_var_internalization_type list ->
+  notation_grammar -> unit
+(** Add a term notation rule to the parsing system. *)
 
-val extend_grammar : all_grammar_command -> unit
+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
 (** For a declared grammar, returns the rule + the ordered entry types
     of variables in the rule (for use in the interpretation) *)
-val recover_notation_grammar :
-  notation -> (precedence * tolerability list) ->
-  notation_var_internalization_type list * notation_grammar
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
 
-(** Adding tactic quotations *)
+(** {5 Adding tactic quotations} *)
 
 val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) ->
   ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 7452f1f452..c8982692b1 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -68,7 +68,7 @@ type tactic_grammar_obj = {
 }
 
 let cache_tactic_notation (_, tobj) =
-  Egramcoq.extend_grammar (Egramcoq.TacticGrammar tobj.tacobj_tacgram);
+  Egramcoq.extend_tactic_grammar tobj.tacobj_tacgram;
   Pptactic.declare_extra_tactic_pprule tobj.tacobj_tacpp
 
 let subst_tactic_parule subst tg =
@@ -769,7 +769,7 @@ let cache_one_syntax_extension se =
     (* Reserve the notation level *)
     Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
-    Egramcoq.extend_grammar (Egramcoq.Notation (prec, se.synext_intern, se.synext_notgram));
+    Egramcoq.extend_constr_grammar prec se.synext_intern se.synext_notgram;
     (* Declare the printing rule *)
     Notation.declare_notation_printing_rule ntn (se.synext_unparsing, fst prec)
 
@@ -1111,7 +1111,7 @@ 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_notation_grammar ntn prec in
+    let typs, pa_rule = Egramcoq.recover_constr_grammar ntn prec in
     { synext_intern = typs;
       synext_level = prec;
       synext_notation = ntn;