From 6b5b4db599333546334bcdbd852be72ddb39d9dc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 11 Oct 2018 18:13:12 +0200
Subject: Deprecating the RAW_TYPED and GLOB_TYPED stanzas of the ARGUMENT
 EXTEND macro.

Those optional arguments did not really make sense. It was pretty clear from
our code base, as all instances where triplicating the same type for TYPED,
RAW_TYPED and GLOB_TYPED.
---
 plugins/funind/g_indfun.ml4 | 2 --
 1 file changed, 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index a2d31780dd..272852d47a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -48,9 +48,7 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
 ARGUMENT EXTEND fun_ind_using
   TYPED AS constr_with_bindings option
   PRINTED BY pr_fun_ind_using_typed
-  RAW_TYPED AS constr_with_bindings_opt
   RAW_PRINTED BY pr_fun_ind_using
-  GLOB_TYPED AS constr_with_bindings_opt
   GLOB_PRINTED BY pr_fun_ind_using
 | [ "using" constr_with_bindings(c) ] -> [ Some c ]
 | [ ] -> [ None ]
-- 
cgit v1.2.3