From 1c6e49ea2bc3f68acd83035332df40921d98c6c2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 27 Sep 2018 01:39:46 +0200
Subject: [ssr] [camlp5] Remove warning from camlp5

Current compilation of ssrparser.ml4 produces:

```
       coqp5 plugins/ssr/ssrparser.ml
Redundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].
```

the solution is easy.
---
 plugins/ssr/ssrparser.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index a7aae5bd31..e4a0910673 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -342,7 +342,7 @@ let interp_index ist gl idx =
 
 open Pltac
 
-ARGUMENT EXTEND ssrindex TYPED AS ssrindex PRINTED BY pr_ssrindex
+ARGUMENT EXTEND ssrindex PRINTED BY pr_ssrindex
   INTERPRETED BY interp_index
 | [ int_or_var(i) ] -> [ mk_index ~loc i ]
 END
-- 
cgit v1.2.3