diff options
Diffstat (limited to 'plugins/subtac/subtac_classes.mli')
| -rw-r--r-- | plugins/subtac/subtac_classes.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index 5b5c02037..5b8636a12 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -16,6 +16,7 @@ open Environ open Nametab open Mod_subst open Topconstr +open Errors open Util open Typeclasses open Implicit_quantifiers |