aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/notation.ml')
-rw-r--r--interp/notation.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml
index b04f3be03..f3ecbd446 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) =
if req = ArgsScopeNoDischarge then None
else Some (req,pop_global_reference r,l)
-let rebuild_arguments_scope (req,r,l) =
+let rebuild_arguments_scope (_,(req,r,l)) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->