From 403c12ac3e8a9c3719aacbfa113600abc74846b7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 09:47:20 +0200
Subject: ssrmatching: avoid warnings about redundant typing clauses in
 ARGUMENT EXTEND

 The warnings were:

 Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND cpattern].
 Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND cpattern].
 Redundant [RAW_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
 Redundant [GLOB_TYPED AS] clause in [ARGUMENT EXTEND lcpattern].
---
 plugins/ssrmatching/ssrmatching.ml4 | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins')

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
 
-- 
cgit v1.2.3