From e925e66c67eb0ff62b26fa4bc5694ea03a573ad9 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Wed, 9 May 2012 12:24:54 +0000
Subject: Tactic unfold always asks for comma between names.

Else the parser takes "at" as a constant to unfold in "unfold plus at ...".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15290 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 79783fd3fa..8b72a5e93f 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -349,7 +349,7 @@ GEXTEND Gram
       | IDENT "lazy"; s = strategy_flag -> Lazy s
       | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
       | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
-      | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
+      | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
       | s = IDENT -> ExtraRedExpr s ] ]
-- 
cgit v1.2.3