Cleaning and documenting Egramcoq.

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

1 files changed, 3 insertions, 3 deletions

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;