diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 1 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c77950c74d..c1b7b63c3e 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -109,7 +109,6 @@ let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (pr_loc let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using - TYPED AS reference_list PRINTED BY pr_firstorder_using_typed RAW_TYPED AS reference_list RAW_PRINTED BY pr_firstorder_using_raw diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index fb053c032f..39f4cf07f3 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -56,7 +56,6 @@ let pr_fun_ind_using_typed prc prlc _ opt_c = ARGUMENT EXTEND fun_ind_using - TYPED AS constr_with_bindings_opt PRINTED BY pr_fun_ind_using_typed RAW_TYPED AS constr_with_bindings_opt RAW_PRINTED BY pr_fun_ind_using |