aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation_ops.ml')
-rw-r--r--interp/notation_ops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b0480aa70..f208b23fb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -687,7 +687,7 @@ let is_onlybinding_meta id metas =
let is_onlybinding_pattern_like_meta isvar id metas =
try match Id.List.assoc id metas with
| _,NtnTypeBinder (NtnBinderParsedAsConstr
- (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+ (AsIdentOrPattern | AsStrictPattern)) -> true
| _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
| _ -> false
with Not_found -> false