From 3b9638f22550c2eaf4da81d7a4aac1633681e565 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 11:29:13 +0000
Subject: Parsing des V8Notation avec motif recursif en v7

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5520 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_constr.ml4 | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 2f606ffd30..280b34c8b5 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -198,7 +198,9 @@ GEXTEND Gram
         IDENT "if"; c1 = constr;
         IDENT "then"; c2 = constr; 
         IDENT "else"; c3 = constr ->
-	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3]) ]
+	  COrderedCase (loc, IfStyle, Some p, c1, [c2; c3])
+      | ".."; c = operconstr LEVEL "0"; ".." ->
+          CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
     | "0" RIGHTA
       [ "?" -> CHole loc
       | "?"; n = Prim.natural -> CPatVar (loc, (false,Pattern.patvar_of_int n))
-- 
cgit v1.2.3