Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: egramml.mli Sprache: SML

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Vernacexpr

(** Mapping of grammar productions to camlp5 actions. *)

(** This is the part specific to vernac extensions.
    For the Coq-level Notation and Tactic Notation, see Egramcoq. *)

type 's grammar_prod_item =
  | GramTerminal of string
  | GramNonTerminal : ('a Genarg.raw_abstract_argument_type *
      ('s, _, 'a) Extend.symbol) Loc.located -> 's grammar_prod_item

val extend_vernac_command_grammar :
  extend_name -> vernac_expr Pcoq.Entry.t option ->
    vernac_expr grammar_prod_item list -> unit

val get_extend_vernac_rule : extend_name -> vernac_expr grammar_prod_item list

val proj_symbol : ('a, 'b, 'c) Extend.ty_user_symbol -> ('a, 'b, 'c) Genarg.genarg_type

(** Utility function reused in Egramcoq : *)

val make_rule :
  (Loc.t -> Genarg.raw_generic_argument list -> 'a) ->
  'a grammar_prod_item list -> 'a Extend.production_rule

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.