diff options
Diffstat (limited to 'tactics/extraargs.ml4')
| -rw-r--r-- | tactics/extraargs.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index dc41cf8e3..a2a8675a8 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -72,9 +72,6 @@ let glob_occs ist l = l let subst_occs evm l = l -type occurrences_or_var = int list or_var -type occurrences = int list - ARGUMENT EXTEND occurrences PRINTED BY pr_int_list_full |