Cleaning and documenting Egramcoq.

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

2 files changed, 17 insertions, 15 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