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 164423ead..46089245c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -467,7 +467,7 @@ let discharge_arguments_scope (_,(req,r,l)) =
if req = ArgsScopeNoDischarge or (isVarRef r & Lib.is_in_section r) then None
else Some (req,Lib.discharge_global r,l)
-let rebuild_arguments_scope (_,(req,r,l)) =
+let rebuild_arguments_scope (req,r,l) =
match req with
| ArgsScopeNoDischarge -> assert false
| ArgsScopeAuto ->