diff options
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 1d5af3ff39..274d3655d3 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -119,7 +119,7 @@ let revert_reserved_type t = then I've introduced a bug... *) let filter _ pat = try - let _ = match_notation_constr false t ([], pat) in + let _ = match_notation_constr ~print_univ:false t ~vars:Id.Set.empty ([], pat) in true with No_match -> false in |