diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extraargs.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ltac/g_auto.ml4 | 2 |
2 files changed, 0 insertions, 4 deletions
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index f4555509cc..0c6d10bf8c 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -285,9 +285,7 @@ let in_clause' = Pltac.in_clause ARGUMENT EXTEND in_clause TYPED AS clause_dft_concl PRINTED BY pr_in_top_clause - RAW_TYPED AS clause_dft_concl RAW_PRINTED BY pr_in_clause - GLOB_TYPED AS clause_dft_concl GLOB_PRINTED BY pr_in_clause | [ in_clause'(cl) ] -> [ cl ] END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 35ed14fc18..8eadb66edc 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -62,9 +62,7 @@ let pr_auto_using _ _ _ = Pptactic.pr_auto_using ARGUMENT EXTEND auto_using TYPED AS uconstr_list PRINTED BY pr_auto_using - RAW_TYPED AS uconstr_list RAW_PRINTED BY pr_auto_using_raw - GLOB_TYPED AS uconstr_list GLOB_PRINTED BY pr_auto_using_glob | [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] | [ ] -> [ [] ] |