diff options
Diffstat (limited to 'toplevel/indschemes.ml')
| -rw-r--r-- | toplevel/indschemes.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 640ef4ab5..3fba117a9 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -27,6 +27,7 @@ open Decl_kinds open Indrec open Declare open Libnames +open Globnames open Goptions open Nameops open Termops |