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
---
 printing/pptactic.ml | 21 ++++++---------------
 1 file changed, 6 insertions(+), 15 deletions(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 0fd3b454ce..04a2ca1e30 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -161,12 +161,9 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
       pr_with_bindings prc prlc (out_gen (rawwit wit_constr_with_bindings) x)
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (rawwit wit_bindings) x)
-  | List0ArgType _ ->
+  | ListArgType _ ->
       hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
-	(fold_list0 (fun a l -> a::l) x []))
-  | List1ArgType _ ->
-      hov 0 (pr_sequence (pr_raw_generic prc prlc prtac prpat prref)
-	(fold_list1 (fun a l -> a::l) x []))
+	(fold_list (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_raw_generic prc prlc prtac prpat prref) (mt()) x)
   | PairArgType _ ->
       hov 0
@@ -203,12 +200,9 @@ let rec pr_glb_generic prc prlc prtac prpat x =
       pr_with_bindings prc prlc (out_gen (glbwit wit_constr_with_bindings) x)
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (glbwit wit_bindings) x)
-  | List0ArgType _ ->
-      hov 0 (pr_sequence (pr_glb_generic prc prlc prtac prpat)
-	(fold_list0 (fun a l -> a::l) x []))
-  | List1ArgType _ ->
+  | ListArgType _ ->
       hov 0 (pr_sequence (pr_glb_generic prc prlc prtac prpat)
-	(fold_list1 (fun a l -> a::l) x []))
+	(fold_list (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_glb_generic prc prlc prtac prpat) (mt()) x)
   | PairArgType _ ->
       hov 0
@@ -239,12 +233,9 @@ let rec pr_top_generic prc prlc prtac prpat x =
       pr_with_bindings prc prlc (c,b)
   | BindingsArgType ->
       pr_bindings_no_with prc prlc (out_gen (topwit wit_bindings) x).Evd.it
-  | List0ArgType _ ->
-      hov 0 (pr_sequence (pr_top_generic prc prlc prtac prpat)
-	(fold_list0 (fun a l -> a::l) x []))
-  | List1ArgType _ ->
+  | ListArgType _ ->
       hov 0 (pr_sequence (pr_top_generic prc prlc prtac prpat)
-	(fold_list1 (fun a l -> a::l) x []))
+	(fold_list (fun a l -> a::l) x []))
   | OptArgType _ -> hov 0 (fold_opt (pr_top_generic prc prlc prtac prpat) (mt()) x)
   | PairArgType _ ->
       hov 0
-- 
cgit v1.2.3