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

1 files changed, 3 insertions, 4 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 76646a4f9..ddaba47b0 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) ] ]
   ;