diff options
Diffstat (limited to 'plugins/ltac/pptactic.mli')
| -rw-r--r-- | plugins/ltac/pptactic.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 5d2a99618..c14874d6c 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -19,6 +19,7 @@ open Environ open Constrexpr open Notation_gram open Tacexpr +open Tactypes type 'a grammar_tactic_prod_item_expr = | TacTerm of string |