diff options
Diffstat (limited to 'vernac/egramcoq.mli')
| -rw-r--r-- | vernac/egramcoq.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli index e15add10f..b0341e6a1 100644 --- a/vernac/egramcoq.mli +++ b/vernac/egramcoq.mli @@ -15,5 +15,5 @@ (** {5 Adding notations} *) -val extend_constr_grammar : Notation_term.one_notation_grammar -> unit +val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) |