diff options
Diffstat (limited to 'plugins/ssrmatching/ssrmatching.ml4')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 2 |
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 |