aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/genarg.ml4
-rw-r--r--interp/genarg.mli2
2 files changed, 3 insertions, 3 deletions
diff --git a/interp/genarg.ml b/interp/genarg.ml
index ac45bfe8dd..b371582a15 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -76,7 +76,7 @@ let exists_argtype s = List.mem s !dyntab
type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
- | IntroWildcard
+ | IntroWildcard of loc
| IntroIdentifier of identifier
| IntroAnonymous
| IntroRewrite of bool
@@ -85,7 +85,7 @@ and case_intro_pattern_expr = intro_pattern_expr list list
let rec pr_intro_pattern = function
| IntroOrAndPattern pll -> pr_case_intro_pattern pll
- | IntroWildcard -> str "_"
+ | IntroWildcard _ -> str "_"
| IntroIdentifier id -> pr_id id
| IntroAnonymous -> str "?"
| IntroRewrite true -> str "->"
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 9773082181..da03718999 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -33,7 +33,7 @@ type 'a with_ebindings = 'a * open_constr bindings
type intro_pattern_expr =
| IntroOrAndPattern of case_intro_pattern_expr
- | IntroWildcard
+ | IntroWildcard of loc
| IntroIdentifier of identifier
| IntroAnonymous
| IntroRewrite of bool