From d3963fc6b6dad5a0cf79815f31b2035ca8b3de25 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Fri, 19 Mar 2021 14:29:07 +0100
Subject: [abbreviation] allow the user to set arguments scope

---
 interp/notation_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/notation_ops.ml')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index ea5e2a1ad4..ced102c703 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -681,7 +681,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
-- 
cgit v1.2.3