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