diff options
Diffstat (limited to 'plugins/ltac/taccoerce.ml')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 27acbb629..6bfa07ee9 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -17,6 +17,7 @@ open Namegen open Tactypes open Genarg open Stdarg +open Tacarg open Geninterp open Pp |