aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4467cf9f2..d125caf54 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -16,6 +16,7 @@ open Namegen
open Libnames
open Impargs
open Glob_term
+open Glob_ops
open Pattern
open Pretyping
open Cases