diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-26 14:35:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-27 00:07:14 +0100 |
| commit | 9b2bb33662a4a1e39202cb81f894b739782c3434 (patch) | |
| tree | a639a0ac146e81ceeb0b075b3551a3f2c3913b9d /parsing/egramcoq.mli | |
| parent | fb50a8aaf8826349ac8c3a90a6d9b354b9cf34ca (diff) | |
Indexing existentially quantified entries returned by interp_entry_name.
Diffstat (limited to 'parsing/egramcoq.mli')
| -rw-r--r-- | parsing/egramcoq.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli index 2b0f7da8c..cdd5fbd0f 100644 --- a/parsing/egramcoq.mli +++ b/parsing/egramcoq.mli @@ -38,7 +38,7 @@ type notation_grammar = { type tactic_grammar = { tacgram_level : int; - tacgram_prods : grammar_prod_item list; + tacgram_prods : Tacexpr.raw_tactic_expr grammar_prod_item list; } (** {5 Adding notations} *) @@ -50,7 +50,7 @@ val extend_tactic_grammar : KerName.t -> tactic_grammar -> unit (** Add a tactic notation rule to the parsing system. This produces a TacAlias tactic with the provided kernel name. *) -val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> grammar_prod_item list list -> unit +val extend_ml_tactic_grammar : Tacexpr.ml_tactic_name -> Tacexpr.raw_tactic_expr grammar_prod_item list list -> unit (** Add a ML tactic notation rule to the parsing system. This produces a TacML tactic with the provided string as name. *) |