diff options
Diffstat (limited to 'parsing/egramcoq.mli')
-rw-r--r-- | parsing/egramcoq.mli | 22 |
1 files changed, 8 insertions, 14 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 6dda3817..e15add10 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -1,25 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open Constrexpr -open Notation_term -open Pcoq -open Extend -open Genarg -open Egramml - -(** Mapping of grammar productions to camlp4 actions *) +(** Mapping of grammar productions to camlp5 actions *) (** This is the part specific to Coq-level Notation and Tactic Notation. For the ML-level tactic and vernac extensions, see Egramml. *) (** {5 Adding notations} *) -val extend_constr_grammar : Notation.level -> Notation_term.notation_grammar -> unit +val extend_constr_grammar : Notation_term.one_notation_grammar -> unit (** Add a term notation rule to the parsing system. *) |