Creation of a new token PATTERNIDENT (?ident) for intro patterns, so

that "intros ? a ? b" behaves as expected.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10155 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 23 insertions, 11 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 10d7f46b57..04e0f84ca3 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -157,7 +157,7 @@ GEXTEND Gram
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
       | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
-      | "@"; "?"; (locid,id) = identref; args=LIST1 identref ->
+      | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
           let args = List.map (fun x -> CRef (Ident x), None) args in
           CApp(loc,(None,CPatVar(locid,(true,id))),args) ]
     | "9"
@@ -222,7 +222,7 @@ GEXTEND Gram
       | n=INT -> CPrim (loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (loc, String s)
       | "_" -> CHole loc
-      | "?"; id=ident -> CPatVar(loc,(false,id)) ] ]
+      | id=pattern_ident -> CPatVar(loc,(false,id)) ] ]
   ;
   fix_constr:
     [ [ fx1=single_fix -> mk_single_fix fx1
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index d2d5ad36a1..8501b34360 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -27,13 +27,19 @@ GEXTEND Gram
   GLOBAL: 
     bigint natural integer identref name ident var preident
     fullyqualid qualid reference dirpath
-    ne_string string;
+    ne_string string pattern_ident pattern_identref;
   preident:
     [ [ s = IDENT -> s ] ]
   ;
   ident:
     [ [ s = IDENT -> id_of_string s ] ]
   ;
+  pattern_ident:
+    [ [ s = PATTERNIDENT -> id_of_string s ] ]
+  ;
+  pattern_identref:
+    [ [ id = pattern_ident -> (loc, id) ] ]
+  ;
   var: (* as identref, but interpret as a term identifier in ltac *)
     [ [ id = ident -> (loc,id) ] ]
   ;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index ff23fb225c..a4f5a4f42a 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -188,7 +188,7 @@ GEXTEND Gram
 	    | t::q -> IntroOrAndPattern [[t;pairify q]]
 	  in pairify tc
       | "_" -> IntroWildcard
-      | "?"; prefix = ident -> IntroFresh prefix
+      | prefix = pattern_ident -> IntroFresh prefix
       | "?" -> IntroAnonymous
       | id = ident -> IntroIdentifier id
       ] ]
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 043a0c08a9..cfa62fa5ad 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -272,7 +272,7 @@ let add_keyword str =
 (* Adding a new token (keyword or special token). *)
 let add_token (con, str) = match con with
   | "" -> add_keyword str
-  | "METAIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
+  | "METAIDENT" | "PATTERNIDENT" | "IDENT" | "FIELD" | "INT" | "STRING" | "EOI"
       -> ()
   | _ ->
       raise (Token.Error ("\
@@ -463,14 +463,16 @@ let process_chars bp c cs =
     | Some t -> (("", t), (bp, ep))
     | None -> err (bp, ep) Undefined_token
 
-(* Parse what follows a dot *)
-let parse_after_dot bp c = parser
+(* Parse what follows a dot/question mark *)
+let parse_after_dot bp c =
+  let constructor = if c = '?' then "PATTERNIDENT" else "FIELD" in
+  parser
   | [< ' ('a'..'z' | 'A'..'Z' | '_' as c); len = ident_tail (store 0 c) >] ->
-      ("FIELD", get_buff len)
+      (constructor, get_buff len)
   | [< s >] ->
       match lookup_utf8 s with
       | Some (Utf8Letter n) -> 
-	  ("FIELD", get_buff (ident_tail (nstore n 0 s) s))
+	  (constructor, get_buff (ident_tail (nstore n 0 s) s))
       | Some (Utf8IdentPart _ | AsciiChar | Utf8Symbol) | None -> 
 	  fst (process_chars bp c s)
 
@@ -481,7 +483,7 @@ let rec next_token = parser bp
   | [< ''$'; len = ident_tail (store 0 '$') >] ep -> 
       comment_stop bp;
       (("METAIDENT", get_buff len), (bp,ep))
-  | [< ''.' as c; t = parse_after_dot bp c >] ep ->
+  | [< ' ('.' | '?') as c; t = parse_after_dot bp c >] ep ->
       comment_stop bp;
       if Options.do_translate() & t=("",".") then between_com := true;
       (t, (bp,ep))
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index b0e573eb91..d72a490467 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -399,6 +399,8 @@ module Prim =
 
     let name = Gram.Entry.create "Prim.name"
     let identref = Gram.Entry.create "Prim.identref"
+    let pattern_ident = Gram.Entry.create "pattern_ident"
+    let pattern_identref = Gram.Entry.create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
     let base_ident = Gram.Entry.create "Prim.base_ident"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index f0d10dcb0a..6515544863 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -132,6 +132,8 @@ module Prim :
     val ident : identifier Gram.Entry.e
     val name : name located Gram.Entry.e
     val identref : identifier located Gram.Entry.e
+    val pattern_ident : identifier Gram.Entry.e
+    val pattern_identref : identifier located Gram.Entry.e
     val base_ident : identifier Gram.Entry.e
     val natural : int Gram.Entry.e
     val bigint : Bigint.bigint Gram.Entry.e
diff --git a/theories/Ints/Z/ZDivModAux.v b/theories/Ints/Z/ZDivModAux.v
index be7955aadd..cb6a01fcd3 100644
--- a/theories/Ints/Z/ZDivModAux.v
+++ b/theories/Ints/Z/ZDivModAux.v
@@ -142,7 +142,7 @@ Hint Resolve Zlt_gt Zle_ge: zarith.
   replace (c * a / b * b) with (c * a - (c * a) mod b).
   rewrite Zmult_minus_distr_l.
   unfold Zminus; apply Zplus_le_compat_l.
-  match goal with |- - ? X <= -?Y => assert (Y <= X); auto with zarith end.
+  match goal with |- - ?X <= -?Y => assert (Y <= X); auto with zarith end.
   apply Zle_trans with ((c mod b) * (a mod b)); auto with zarith.
   rewrite Zmod_mult; case (Zmod_le_first ((c mod b) * (a mod b)) b); 
     auto with zarith.