aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d45e6b9b3..62b8cdcea 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -23,6 +23,7 @@ open Libnames
open Impargs
open Topconstr
open Glob_term
+open Glob_ops
open Pattern
open Nametab
open Notation
@@ -876,7 +877,7 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
- let loc = Glob_term.loc_of_glob_constr t in
+ let loc = Glob_ops.loc_of_glob_constr t in
try
(* Adjusts to the number of arguments expected by the notation *)
let (t,args,argsscopes,argsimpls) = match t,n with