diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 46 |
1 files changed, 26 insertions, 20 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 18eb3eed34..74b7bcc93f 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -105,12 +105,37 @@ type grammar_object (** Type of reinitialization data *) type gram_reinit = gram_assoc * gram_position +(** General entry keys *) + +(** This intermediate abstract representation of entries can + both be reified into mlexpr for the ML extensions and + dynamically interpreted as entries for the Coq level extensions +*) + +type ('self, 'a) entry_key = ('self, 'a) Extend.symbol = +| Atoken : Tok.t -> ('self, Tok.t) entry_key +| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key +| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key +| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key +| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key +| Aself : ('self, 'self) entry_key +| Anext : ('self, 'self) entry_key +| Aentry : 'a Entry.t -> ('self, 'a) entry_key +| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key + (** Add one extension at some camlp4 position of some camlp4 entry *) -val grammar_extend : +val unsafe_grammar_extend : grammar_object Gram.entry -> gram_reinit option (** for reinitialization if ever needed *) -> Gram.extend_statment -> unit +val grammar_extend : + 'a Gram.entry -> + gram_reinit option (** for reinitialization if ever needed *) -> + 'a Extend.extend_statment -> unit + (** Remove the last n extensions *) val remove_grammars : int -> unit @@ -253,25 +278,6 @@ val symbol_of_constr_prod_entry_key : gram_assoc option -> constr_entry_key -> bool -> constr_prod_entry_key -> Gram.symbol -(** General entry keys *) - -(** This intermediate abstract representation of entries can - both be reified into mlexpr for the ML extensions and - dynamically interpreted as entries for the Coq level extensions -*) - -type ('self, _) entry_key = -| Alist1 : ('self, 'a) entry_key -> ('self, 'a list) entry_key -| Alist1sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key -| Alist0 : ('self, 'a) entry_key -> ('self, 'a list) entry_key -| Alist0sep : ('self, 'a) entry_key * string -> ('self, 'a list) entry_key -| Aopt : ('self, 'a) entry_key -> ('self, 'a option) entry_key -| Amodifiers : ('self, 'a) entry_key -> ('self, 'a list) entry_key -| Aself : ('self, 'self) entry_key -| Anext : ('self, 'self) entry_key -| Aentry : 'a Entry.t -> ('self, 'a) entry_key -| Aentryl : 'a Entry.t * int -> ('self, 'a) entry_key - val name_of_entry : 'a Gram.entry -> 'a Entry.t (** Binding general entry keys to symbols *) |