diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 933e2baee3..814e3a4d5a 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -1039,8 +1039,8 @@ ARGUMENT EXTEND cpattern PRINTED BY pr_ssrterm INTERPRETED BY interp_ssrterm GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm - GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm | [ "Qed" constr(c) ] -> [ mk_lterm c ] END @@ -1058,8 +1058,8 @@ ARGUMENT EXTEND lcpattern PRINTED BY pr_ssrterm INTERPRETED BY interp_ssrterm GLOBALIZED BY glob_cpattern SUBSTITUTED BY subst_ssrterm - RAW_TYPED AS cpattern RAW_PRINTED BY pr_ssrterm - GLOB_TYPED AS cpattern GLOB_PRINTED BY pr_ssrterm + RAW_PRINTED BY pr_ssrterm + GLOB_PRINTED BY pr_ssrterm | [ "Qed" lconstr(c) ] -> [ mk_lterm c ] END |