diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3723504149..70eb211067 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -19,7 +19,7 @@ open Genredexpr (** The parser of Coq *) -module Gram : Compat.GrammarSig +module Gram : module type of Compat.GrammarMake(CLexer) (** The parser of Coq is built from three kinds of rule declarations: @@ -128,7 +128,6 @@ val uconstr : gram_universe val utactic : gram_universe val uvernac : gram_universe -val set_grammar : 'a Entry.t -> 'a Gram.entry -> unit val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry @@ -234,8 +233,6 @@ val main_entry : (Loc.t * vernac_expr) option Gram.entry val get_command_entry : unit -> vernac_expr Gram.entry val set_command_entry : vernac_expr Gram.entry -> unit -val name_of_entry : 'a Gram.entry -> 'a Entry.t - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** Binding general entry keys to symbols *) |