diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-14 18:59:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-14 19:08:16 +0200 |
| commit | 87a81fd7e6ff6b45c76690471eb671ba4b005338 (patch) | |
| tree | 74c6322d95552effca6a9bb1b92befdd768394ea /intf | |
| parent | f0f3d650ec4fcd1644811e099f0f3f50d660a992 (diff) | |
Moving and enhancing the grammar_tactic_prod_item_expr type.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 14a80379e..ae9328fcc 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -200,10 +200,6 @@ type one_inductive_expr = type proof_expr = plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) -type grammar_tactic_prod_item_expr = - | TacTerm of string - | TacNonTerm of Loc.t * string * (Names.Id.t * string) - type syntax_modifier = | SetItemLevel of string list * Extend.production_level | SetLevel of int |