From fe0a1f5e856b702a5e4638e22b748d2d8af475c2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 10:53:49 +0000
Subject: Utilisation de '..' pour la notation concrete des motifs recursifs de
 filtrage

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

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index bf4c3372ef..3df5253e6f 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -181,7 +181,7 @@ GEXTEND Gram
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
     | "9"
-        [ ".."; ".."; c = operconstr LEVEL "0"; ".."; ".." ->
+        [ ".."; c = operconstr LEVEL "0"; ".." ->
           CAppExpl (loc,(None,Ident (loc,Topconstr.ldots_var)),[c]) ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 75222eaa43..2f6b6961c0 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -64,7 +64,7 @@ GEXTEND Gram
   subgoal_command:
     [ [ c = check_command; "." -> c
       | tac = Tactic.tactic;
-        use_dft_tac = [ "." -> false | ".."; "." -> true ] ->
+        use_dft_tac = [ "." -> false | "..." -> true ] ->
           (fun g ->
             let g = match g with Some gl -> gl | _ -> 1 in
             VernacSolve(g,tac,use_dft_tac)) ] ]
-- 
cgit v1.2.3