diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 82f030ae0..b241336e7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -42,6 +42,7 @@ open Recordops open Evarutil open Pretype_errors open Glob_term +open Glob_ops open Evarconv open Pattern open Misctypes |