diff options
Diffstat (limited to 'pretyping/glob_term.ml')
| -rw-r--r-- | pretyping/glob_term.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index a736e6eec..5922d38dc 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -7,6 +7,8 @@ (************************************************************************) (*i*) +open Errors +open Pp open Util open Names open Sign |