aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_termops.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/glob_termops.mli')
-rw-r--r--plugins/funind/glob_termops.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 80a8811f1..761337b07 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,4 +1,5 @@
open Glob_term
+open Misctypes
(* Ocaml 3.06 Map.S does not handle is_empty *)
val idmap_is_empty : 'a Names.Idmap.t -> bool