From ae06af990c17e462ecc39ef048d664a34e3e2d7d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 16 Jan 2006 08:51:22 +0000
Subject: cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7874 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 3 ++-
 parsing/pptactic.ml  | 2 +-
 2 files changed, 3 insertions(+), 2 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d396854ba7..f27191e2ec 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -155,7 +155,8 @@ GEXTEND Gram
   ;
   simple_intropattern:
     [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc
-      | "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
+      | "("; tc = LIST0 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc]
+      | "()" -> IntroOrAndPattern [[]]
       | "_" -> IntroWildcard
       | id = ident -> IntroIdentifier id
       ] ]
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index c2029dde5b..46caf88b82 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -354,7 +354,7 @@ let rec pr_intro_pattern = function
   | IntroWildcard -> str "_"
   | IntroIdentifier id -> pr_id id
 and pr_case_intro_pattern = function
-  | [_::_ as pl] ->
+  | [pl] ->
       str "(" ++ hov 0 (prlist_with_sep pr_coma pr_intro_pattern pl) ++ str ")"
   | pll ->
       str "[" ++
-- 
cgit v1.2.3