Better parsing of typeclasses, any constr is allowed for ! bindings so

notations work and bug #1846 gets completely fixed.


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

3 files changed, 17 insertions, 27 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index cf37efc77a..f6bd4fae3e 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -185,7 +185,11 @@ let full_class_binders env l =
     List.fold_left (fun (l', avoid) (iid, bk, cl as x) -> 
       match bk with
 	  Implicit -> 
-	    let (loc, id, l) = destClassAppExpl cl in
+	    let (loc, id, l) = 
+	      try destClassAppExpl cl 
+	      with Not_found -> 
+		user_err_loc (constr_loc cl, "class_binders", str"Not an applied type class")
+	    in
 	    let gr = Nametab.global id in
 	      (try
 		  let c = class_info gr in
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 277d8b3c8c..ea8d532f95 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -112,8 +112,8 @@ let impl_ident =
 	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
     
-let ident_eq =
-  Gram.Entry.of_parser "ident_eq"
+let ident_colon =
+  Gram.Entry.of_parser "ident_colon"
     (fun strm ->
       match Stream.npeek 1 strm with
 	| [("IDENT",s)] ->
@@ -438,29 +438,16 @@ GEXTEND Gram
 	LocalRawAssum ([n], TypeClass bk, t)
     ] ]
   ;
-  typeclass_constraint:
-    [ [ "!" ; qid=global ; cl = LIST0 typeclass_param -> 
-	(loc, Anonymous), Explicit, CApp (loc, (None, mkRefC qid), cl)
-    | iid=ident_eq ; qid=typeclass_name ; cl = LIST0 typeclass_param -> 
-	(loc, Name iid), (fst qid), CApp (loc, (None, mkRefC (snd qid)), cl)
-    | qid=global ; cl = LIST0 typeclass_param -> 
-	(loc, Anonymous), Implicit, CApp (loc, (None, mkRefC qid), cl)
-    ] ]
-  ;
-  typeclass_name:
-    [ [ id=global -> (Implicit, id)
-    | "!"; id=global -> (Explicit, id)
-    ] ]
-  ;
 
-  typeclass_param: 
-    [ [ id = global -> CRef id, None
-    | c = sort -> CSort (loc, c), None
-    | id = lpar_id_coloneq; c=lconstr; ")" ->
-	(c,Some (loc,ExplByName id))
-    | c=operconstr LEVEL "9" -> c, None
+  typeclass_constraint:
+    [ [ "!" ; c = operconstr LEVEL "200" -> (loc, Anonymous), Explicit, c
+    | iid=ident_colon ; expl = [ "!" -> Explicit | -> Implicit ] ; c = operconstr LEVEL "200" ->
+	(loc, Name iid), expl, c
+    | c = operconstr LEVEL "200" ->
+	(loc, Anonymous), Implicit, c
     ] ]
   ;
+  
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 76646a4f97..ddaba47b0b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -275,10 +275,9 @@ GEXTEND Gram
               | None -> 
 		  (* If there is only one argument, it is the recursive one, 
 		     otherwise, we search the recursive index later *)
-		  if List.length names = 1 then
-		    let (loc, na) = List.hd names in
-		      Some (loc, Nameops.out_name na)
-		  else None	  
+		  match names with
+		    | [(loc, Name na)] -> Some (loc, na)
+		    | _ -> None	  
 	  in 
 	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;