aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssrmatching
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ssrmatching')
-rw-r--r--plugins/ssrmatching/ssrmatching.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index bedf925e8..c265103a6 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -904,7 +904,7 @@ let pr_ssrpattern_roundp _ _ _ = pr_pattern_roundp
let wit_rpatternty = add_genarg "rpatternty" pr_pattern
let glob_ssrterm gs = function
- | k, (_, Some c) as x -> k,
+ | k, (_, Some c) -> k,
let x = Tacintern.intern_constr gs c in
fst x, Some c
| ct -> ct