aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/egramcoq.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/egramcoq.ml')
-rw-r--r--parsing/egramcoq.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index d51b8b54e..7f50fd22a 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -440,7 +440,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function
CAst.make ~loc @@ CNotation (notation , env)
| ForPattern -> fun notation loc env ->
let invalid = List.exists (fun (_, b) -> not b) env.binders in
- let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in
+ let () = if invalid then Constrexpr_ops.error_invalid_pattern_notation ~loc () in
let env = (env.constrs, env.constrlists) in
CAst.make ~loc @@ CPatNotation (notation, env, [])