diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 34 |
1 files changed, 10 insertions, 24 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 387a62604..36e5e420a 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -10,12 +10,10 @@ open Names open Extend -open Vernacexpr open Genarg open Constrexpr open Libnames open Misctypes -open Genredexpr (** The parser of Coq *) @@ -89,6 +87,12 @@ module type S = end with type 'a Entry.e = 'a Grammar.GMake(CLexer).Entry.e +module Symbols : sig + + val stoken : Tok.t -> Gram.symbol + val snterm : Gram.internal_entry -> Gram.symbol +end + (** The parser of Coq is built from three kinds of rule declarations: - dynamic rules declared at the evaluation of Coq files (using @@ -177,11 +181,14 @@ val map_entry : ('a -> 'b) -> 'a Gram.entry -> 'b Gram.entry type gram_universe val get_univ : string -> gram_universe +val create_universe : string -> gram_universe + +val new_entry : gram_universe -> string -> 'a Gram.entry val uprim : gram_universe val uconstr : gram_universe val utactic : gram_universe -val uvernac : gram_universe + val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry -> unit val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Gram.entry @@ -249,27 +256,6 @@ module Module : val module_type : module_ast Gram.entry end -module Vernac_ : - sig - val gallina : vernac_expr Gram.entry - val gallina_ext : vernac_expr Gram.entry - val command : vernac_expr Gram.entry - val syntax : vernac_expr Gram.entry - val vernac_control : vernac_control Gram.entry - val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val noedit_mode : vernac_expr Gram.entry - val command_entry : vernac_expr Gram.entry - val red_expr : raw_red_expr Gram.entry - val hint_info : Typeclasses.hint_info_expr Gram.entry - end - -(** The main entry: reads an optional vernac command *) -val main_entry : (Loc.t * vernac_control) option Gram.entry - -(** Handling of the proof mode entry *) -val get_command_entry : unit -> vernac_expr Gram.entry -val set_command_entry : vernac_expr Gram.entry -> unit - val epsilon_value : ('a -> 'self) -> ('self, 'a) Extend.symbol -> 'self option (** {5 Extending the parser without synchronization} *) |