From 21b90199c995163145daf447f67dd24cbb591e1d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 18 Mar 2012 13:57:02 +0000
Subject: 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
---
 tactics/extraargs.ml4 | 20 +++-----------------
 1 file changed, 3 insertions(+), 17 deletions(-)

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 72e18ab140..aa9e990cbe 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
 
-- 
cgit v1.2.3