From a0ea7fc67d18598e88559a133cac6b1d993ec66c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:54:54 +0000
Subject: Bug affichage

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

diff --git a/tactics/Refine.v b/tactics/Refine.v
index 33d6d9cab1..fe421497ff 100644
--- a/tactics/Refine.v
+++ b/tactics/Refine.v
@@ -7,4 +7,4 @@ Grammar tactic simple_tactic: ast :=
   tcc [ "Refine" castedopenconstrarg($c) ] -> [(Tcc $c)].
 
 Syntax tactic level 0:
-  tcc [(Tcc $C)] -> ["Refine " $C].
+  tcc [ (Refine $C) ] -> ["Refine " $C].
-- 
cgit v1.2.3