diff options
Diffstat (limited to 'plugins/ltac/pltac.mli')
| -rw-r--r-- | plugins/ltac/pltac.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index de23d2f8e..a75ca8ecb 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -16,6 +16,7 @@ open Constrexpr open Tacexpr open Genredexpr open Misctypes +open Tactypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry |