diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /parsing/egramml.mli | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'parsing/egramml.mli')
-rw-r--r-- | parsing/egramml.mli | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/parsing/egramml.mli b/parsing/egramml.mli index f71c368a..1ad94720 100644 --- a/parsing/egramml.mli +++ b/parsing/egramml.mli @@ -6,24 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Vernacexpr + (** Mapping of grammar productions to camlp4 actions. *) (** This is the part specific to vernac extensions. For the Coq-level Notation and Tactic Notation, see Egramcoq. *) -type grammar_prod_item = +type 's grammar_prod_item = | GramTerminal of string - | GramNonTerminal of Loc.t * Genarg.argument_type * - Pcoq.prod_entry_key * Names.Id.t option + | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type * + ('s, 'a) Extend.symbol -> 's grammar_prod_item val extend_vernac_command_grammar : - Vernacexpr.extend_name -> Vernacexpr.vernac_expr Pcoq.Gram.entry option -> - grammar_prod_item list -> unit + Vernacexpr.extend_name -> vernac_expr Pcoq.Gram.entry option -> + vernac_expr grammar_prod_item list -> unit -val get_extend_vernac_rule : Vernacexpr.extend_name -> grammar_prod_item list +val get_extend_vernac_rule : Vernacexpr.extend_name -> vernac_expr grammar_prod_item list (** Utility function reused in Egramcoq : *) val make_rule : - (Loc.t -> (Names.Id.t * Genarg.raw_generic_argument) list -> 'b) -> - grammar_prod_item list -> Pcoq.Gram.symbol list * Pcoq.Gram.action + (Loc.t -> Genarg.raw_generic_argument list -> 'a) -> + 'a grammar_prod_item list -> 'a Extend.production_rule |