From dca676a77ecc68240ad7beb1342ea1ff8963efb3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 12 Nov 2003 19:32:13 +0000
Subject: Suppression du "..." final !

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

diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 91e765dc4a..a3c92311cf 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -28,7 +28,7 @@ open Vernac_
 open Module
 
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "..."; "where"; "at" ]
+let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
 let _ = 
   if not !Options.v7 then
     List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
@@ -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