aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind/glob_term_to_relation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind/glob_term_to_relation.ml')
-rw-r--r--plugins/funind/glob_term_to_relation.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index f18309d04..ccf2caaf5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -3,6 +3,7 @@ open Pp
open Names
open Term
open Glob_term
+open Glob_ops
open Libnames
open Indfun_common
open Errors