Fix typeclass constraint grammar rule to allow `{_ : Reflexive A R}.

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

1 files changed, 11 insertions, 5 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5d5f6e4d4..ad9cba880 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -95,15 +95,21 @@ let impl_ident_head =
 	      | _ -> err ())
 	| _ -> err ())
 
-let ident_colon =
-  Gram.Entry.of_parser "ident_colon"
+let name_colon =
+  Gram.Entry.of_parser "name_colon"
     (fun strm ->
       match get_tok (stream_nth 0 strm) with
 	| IDENT s ->
             (match get_tok (stream_nth 1 strm) with
               | KEYWORD ":" ->
                   stream_njunk 2 strm;
-                  Names.id_of_string s
+                  Name (Names.id_of_string s)
+              | _ -> err ())
+	| KEYWORD "_" ->
+          (match get_tok (stream_nth 1 strm) with
+              | KEYWORD ":" ->
+                  stream_njunk 2 strm;
+                  Anonymous
               | _ -> err ())
         | _ -> err ())
 
@@ -421,8 +427,8 @@ GEXTEND Gram
     [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), true, c
       | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
 	  id, expl, c
-      | iid=ident_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
-	  (loc, Name iid), expl, c
+      | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" ->
+	  (loc, iid), expl, c
       | c = operconstr LEVEL "200" ->
 	  (loc, Anonymous), false, c
     ] ]