diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-18 13:57:02 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-03-18 13:57:02 +0000 |
| commit | 21b90199c995163145daf447f67dd24cbb591e1d (patch) | |
| tree | 321968f47f642d5bdfd3a6fe1e450dc13ad10b1d | |
| parent | 2d0e7cca0227a935b43e8afe08330af8d7c3a5c3 (diff) | |
Removing redundant entry int_nelist and removing extra space when
printing occurrences list.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15044 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/extraargs.ml4 | 20 |
1 files changed, 3 insertions, 17 deletions
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4 index 72e18ab14..aa9e990cb 100644 --- a/tactics/extraargs.ml4 +++ b/tactics/extraargs.ml4 @@ -33,23 +33,9 @@ END let pr_orient = pr_orient () () () -let pr_int_list_full _prc _prlc _prt l = - let rec aux = function - | i :: l -> Pp.int i ++ Pp.spc () ++ aux l - | [] -> Pp.mt() - in aux l -ARGUMENT EXTEND int_nelist - PRINTED BY pr_int_list_full - RAW_TYPED AS int list - RAW_PRINTED BY pr_int_list_full - GLOB_TYPED AS int list - GLOB_PRINTED BY pr_int_list_full -| [ integer(x) int_nelist(l) ] -> [x::l] -| [ integer(x) ] -> [ [x] ] -END - -let pr_int_list = pr_int_list_full () () () +let pr_int_list = Pp.pr_sequence Pp.int +let pr_int_list_full _prc _prlc _prt l = pr_int_list l open Glob_term @@ -93,7 +79,7 @@ ARGUMENT EXTEND occurrences GLOB_TYPED AS occurrences_or_var GLOB_PRINTED BY pr_occurrences -| [ int_nelist(l) ] -> [ ArgArg l ] +| [ ne_integer_list(l) ] -> [ ArgArg l ] | [ var(id) ] -> [ ArgVar id ] END |