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

2 files changed, 12 insertions, 6 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5d5f6e4d45..ad9cba880b 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
     ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ac81786b6f..814ff9a397 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -143,7 +143,7 @@ let test_plurial_form_types = function
 (* Gallina declarations *)
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion
-    typeclass_constraint record_field decl_notation rec_definition;
+    record_field decl_notation rec_definition;
 
   gallina:
       (* Definition, Theorem, Variable, Axiom, ... *)