aboutsummaryrefslogtreecommitdiff
path: root/interp/stdarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/stdarg.ml')
-rw-r--r--interp/stdarg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..c0dd9e45c4 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,7 +34,7 @@ let wit_pre_ident : string uniform_genarg_type =
let loc_of_or_by_notation f = function
| AN c -> f c
- | ByNotation (loc,s,_) -> loc
+ | ByNotation (loc,(s,_)) -> loc
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"