diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 448881dcf9..f208b23fb6 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -13,6 +13,7 @@ open CErrors open Util open Names open Nameops +open Constr open Globnames open Decl_kinds open Misctypes @@ -686,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 |