diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 |
1 files changed, 0 insertions, 2 deletions
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 ] |