From a778b72e3ebfbe784fbe55ee5e124ba3f66cfb10 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Fri, 5 Jul 2013 01:49:27 +0000
Subject: Expurgating the useless difference between List0 and List1 at the
 level of generic arguments. This only matters at parsing time.

TODO: the current status is not satisfactory enough, as rule
emptyness is still decided w.r.t. generic arguments. This should be
done on a grammar entry basis instead.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16617 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/top_printers.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 9d6b4886b5..6d90af997d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -366,8 +366,7 @@ let rec pr_argument_type = function
   | ConstrWithBindingsArgType -> str"constr-with-bindings"
   | BindingsArgType -> str"bindings"
   | RedExprArgType -> str"redexp"
-  | List0ArgType t -> pr_argument_type t ++ str" list0"
-  | List1ArgType t -> pr_argument_type t ++ str" list1"
+  | ListArgType t -> pr_argument_type t ++ str" list"
   | OptArgType t -> pr_argument_type t ++ str" opt"
   | PairArgType (t1,t2) ->
       str"("++ pr_argument_type t1 ++ str"*" ++ pr_argument_type t2 ++str")"
-- 
cgit v1.2.3