- Fixed bug 2058 (as much as possible - the syntax of "pose (f binders := ...)"

  is not so robust).
- Updating CHANGES


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

2 files changed, 6 insertions, 5 deletions

diff --git a/CHANGES b/CHANGES
index dc7efbab35..b0b7f62e96 100644
--- a/CHANGES
+++ b/CHANGES
@@ -11,7 +11,7 @@ Tactics
   incompatibilities solvable by redefining "intuition" as 
   "unfold iff in *; intuition".
 - Improved support of dependent goals over objects in dependent types for
-  "destruct".
+  "destruct" (rare source of incompatibility).
 
 Vernacular commands
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index a531770a46..e370b693f0 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -72,15 +72,16 @@ let test_lpar_id_colon =
 let check_for_coloneq =
   Gram.Entry.of_parser "lpar_id_colon"
     (fun strm ->
-      let rec skip_to_rpar n =
+      let rec skip_to_rpar p n =
 	match list_last (Stream.npeek n strm) with
-        | ("",")") -> n+1
+        | ("","(") -> skip_to_rpar (p+1) (n+1)
+        | ("",")") -> if p=0 then n+1 else skip_to_rpar (p-1) (n+1)
 	| ("",".") -> raise Stream.Failure
-	| _ -> skip_to_rpar (n+1) in
+	| _ -> skip_to_rpar p (n+1) in
       let rec skip_names n =
 	match list_last (Stream.npeek n strm) with
         | ("IDENT",_) | ("","_") -> skip_names (n+1)
-	| ("",":") -> skip_to_rpar (n+1) (* skip a constr *)
+	| ("",":") -> skip_to_rpar 0 (n+1) (* skip a constr *)
 	| _ -> raise Stream.Failure in
       let rec skip_binders n =
 	match list_last (Stream.npeek n strm) with