From 5520db62486ad628f91737833623aa69c4c1b8af Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 6 Jun 2016 20:16:32 +0200
Subject: Removing the use to Egramcoq.recover_constr_grammar.

---
 interp/notation.mli | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 480979ccc3..a85dc50f2f 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -196,10 +196,11 @@ val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmd
 (** Declare and look for the printing rule for symbolic notations *)
 type unparsing_rule = unparsing list * precedence
 type extra_unparsing_rules = (string * string) list
-val declare_notation_printing_rule :
-  notation -> extra:extra_unparsing_rules -> unparsing_rule -> unit
+val declare_notation_rule :
+  notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
 val find_notation_printing_rule : notation -> unparsing_rule
 val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
 val add_notation_extra_printing_rule : notation -> string -> string -> unit
 
 (** Rem: printing rules for primitive token are canonical *)
-- 
cgit v1.2.3