diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-31 18:42:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-31 19:32:40 +0200 |
| commit | b5de86be330f6c878b8f12173d46a4c250fac755 (patch) | |
| tree | bef5f918c3e40cdbccee9870b7a6c82aa8e5c6a2 /ltac/tacentries.mli | |
| parent | 63cef1ee8de62312df9afc2d515578df9c4cb9b1 (diff) | |
Moving the code handling tactic notations to Tacentries.
Diffstat (limited to 'ltac/tacentries.mli')
| -rw-r--r-- | ltac/tacentries.mli | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/ltac/tacentries.mli b/ltac/tacentries.mli index 3cf0bc5cc..b60d8f478 100644 --- a/ltac/tacentries.mli +++ b/ltac/tacentries.mli @@ -19,3 +19,11 @@ val add_ml_tactic_notation : ml_tactic_name -> Tacexpr.raw_tactic_expr Egramml.grammar_prod_item list list -> unit val register_ltac : bool -> Vernacexpr.tacdef_body list -> unit + +(** {5 Adding tactic quotations} *) + +val create_ltac_quotation : string -> + ('grm Loc.located -> raw_tactic_arg) -> ('grm Pcoq.Gram.entry * int option) -> unit +(** [create_ltac_quotation name f e] adds a quotation rule to Ltac, that is, + Ltac grammar now accepts arguments of the form ["name" ":" "(" <e> ")"], and + generates an argument using [f] on the entry parsed by [e]. *) |