diff options
Diffstat (limited to 'pretyping/glob_ops.ml')
| -rw-r--r-- | pretyping/glob_ops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7804cc6796..055fd68f6c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,6 +13,7 @@ open Globnames open Misctypes open Glob_term open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) |