From 21ef8f6d6679c0f6865313eb5c0dec166a5fdb61 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 6 Mar 2008 15:16:31 +0000
Subject: repair for commit 10612 (due to grammar order, some syntaxes weren't
 working) and add a simpler synonym for "exactly N times" :  rewrite 3 H  (or
 rewrite 3H) means rewrite 3!H

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10629 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex |  4 ++--
 parsing/g_tactic.ml4      | 14 ++++++++------
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6a794e9eb3..342b20cb57 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1828,8 +1828,8 @@ This happens if \term$_1$ does not occur in the goal.
    $n$ rewrites. 
   \item {\tt !} : works as {\tt ?}, except that at least one rewrite 
     should succeed, otherwise the tactic fails. 
-  \item {\tt $n$!} : precisely $n$ rewrites of $\term$ will be done, 
-    leading to failure if these $n$ rewrites are not possible. 
+  \item {\tt $n$!} (or simply {\tt $n$}) : precisely $n$ rewrites 
+    of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. 
   \end{itemize}
 
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 2e515a9a6d..a4e5d4cb83 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -323,19 +323,21 @@ GEXTEND Gram
     [ [ id1 = id_or_meta; IDENT "into"; id2 = id_or_meta -> (id1,id2) ] ]
   ;
   rewriter : 
-    [ [ c = constr_with_bindings -> (Precisely 1, c)
-      | "!"; c = constr_with_bindings -> (RepeatPlus,c)
-      |	"?"; c = constr_with_bindings -> (RepeatStar,c)
-      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
-      |	n = natural; "?"; c = constr_with_bindings -> (UpTo n,c)
+    [ [ 
     (* hack for allowing "rewrite ?t" and "rewrite NN?t" that normally 
        produce a pattern_ident *)
-      | c = pattern_ident -> 
+        c = pattern_ident -> 
 	  let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in  
 	  (RepeatStar, c)
       | n = natural; c = pattern_ident -> 
 	  let c = (CRef (Libnames.Ident (loc,c)), NoBindings) in  
 	  (UpTo n, c)
+      | "!"; c = constr_with_bindings -> (RepeatPlus,c)
+      |	"?"; c = constr_with_bindings -> (RepeatStar,c)
+      | n = natural; "!"; c = constr_with_bindings -> (Precisely n,c)
+      |	n = natural; "?"; c = constr_with_bindings -> (UpTo n,c)
+      | n = natural; c = constr_with_bindings -> (Precisely n,c)
+      | c = constr_with_bindings -> (Precisely 1, c)
       ] ]
   ;
   oriented_rewriter : 
-- 
cgit v1.2.3