aboutsummaryrefslogtreecommitdiff
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 ea95655c18..313a9e85a4 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -680,7 +680,7 @@ let check_variables_and_reversibility nenv
str " position as part of a recursive pattern.") in
let check_type x typ =
match typ with
- | NtnInternTypeAny ->
+ | NtnInternTypeAny _ ->
begin
try check_pair "term" x (Id.Map.find x recvars) foundrec
with Not_found -> check_bound x