diff options
author | 2016-05-10 09:59:41 +0200 | |
---|---|---|
committer | 2016-05-10 19:28:24 +0200 | |
commit | 810afe7c16ca2d18ac7fb39b1d3bd1a3db1c1331 (patch) | |
tree | 3f0e5d4cb1186f2e68e2635020c5247dc01d12e3 /parsing/pcoq.mli | |
parent | 61f79019be6082c3ebabd503c322fb2edb05a99a (diff) |
Type-safe constr notations.
This removes the last call to unsafe_grammar_extend, so that all handwritten
grammar extensions are now type-safe. Grammars defined by CAMLPX EXTEND are
still using the unsafe interface, but as they insert explicit casts they are
deemed safe.
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r-- | parsing/pcoq.mli | 36 |
1 files changed, 0 insertions, 36 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8d653a179..84f72ac55 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -254,39 +254,3 @@ val synchronize_level_positions : unit -> unit val register_empty_levels : bool -> int list -> gram_level list val remove_levels : int -> unit - -(** {5 Unsafe grammar extension API} - -For compatibility purpose only. Do not use in newly written code. - -*) - -val gram_token_of_token : Tok.t -> Gram.symbol -val gram_token_of_string : string -> Gram.symbol -val level_of_snterml : Gram.symbol -> int - -(** The superclass of all grammar entries *) -type grammar_object - -(** Binding constr entry keys to entries and symbols *) - -val interp_constr_entry_key : bool (** true for cases_pattern *) -> - int -> grammar_object Gram.entry * int option - -val symbol_of_constr_prod_entry_key : gram_assoc option -> - constr_entry_key -> bool -> constr_prod_entry_key -> - Gram.symbol - -type unsafe_single_extend_statment = - string option * - gram_assoc option * - Gram.production_rule list - -type unsafe_extend_statment = - gram_position option * - unsafe_single_extend_statment list - -val unsafe_grammar_extend : - grammar_object Gram.entry -> - gram_reinit option (** for reinitialization if ever needed *) -> - unsafe_extend_statment -> unit |