Fix bugs #1975 and #1976.

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

2 files changed, 13 insertions, 16 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f726f8992..4daf21955 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -157,7 +157,12 @@ let binder_list_of_ids ids =
   List.map (fun id -> LocalRawAssum ([dummy_loc, Name id], Default Implicit, CHole (dummy_loc, None))) ids
       
 let next_ident_away_from id avoid = make_fresh avoid (Global.env ()) id
-    
+
+let next_name_away_from na avoid = 
+  match na with
+  | Anonymous -> make_fresh avoid (Global.env ()) (id_of_string "anon")
+  | Name id -> make_fresh avoid (Global.env ()) id
+
 let combine_params avoid fn applied needed =
   let named, applied = 
     List.partition 
@@ -182,7 +187,7 @@ let combine_params avoid fn applied needed =
       | (x, None) :: app, (None, (Name id, _, _)) :: need ->
 	  aux (x :: ids) avoid app need
 	    
-      | _, (Some cl, (Name id, _, _) as d) :: need -> 
+      | _, (Some cl, (_, _, _) as d) :: need -> 
 	  let t', avoid' = fn avoid d in
 	    aux (t' :: ids) avoid' app need
 
@@ -192,15 +197,14 @@ let combine_params avoid fn applied needed =
 	  let t', avoid' = fn avoid decl in
 	    aux (t' :: ids) avoid' app need
 
-      | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
-
-      | _, _ -> raise (Invalid_argument "combine_params")
+      | (x,_) :: _, [] -> 
+	  user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
-
+    
 let combine_params_freevar avoid applied needed =
   combine_params avoid
-    (fun avoid (_, (id, _, _)) -> 
-      let id' = next_ident_away_from (Nameops.out_name id) avoid in
+    (fun avoid (_, (na, _, _)) -> 
+      let id' = next_name_away_from na avoid in
 	(CRef (Ident (dummy_loc, id')), Idset.add id' avoid))
     applied needed
 
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 702d9efb0..301f9bf2a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -123,14 +123,6 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true))
     1 (List.rev (Anonymous :: (List.map pi1 ctx)))
 
-let degenerate_decl (na,b,t) =
-  let id = match na with
-    | Name id -> id
-    | Anonymous -> anomaly "Unnamed record variable" in 
-  match b with
-    | None -> (id, Entries.LocalAssum t)
-    | Some b -> (id, Entries.LocalDef b)
-
 let name_typeclass_binder avoid = function
   | LocalRawAssum ([loc, Anonymous], bk, c) ->
       let name = 
@@ -157,6 +149,7 @@ let new_class id par ar sup props =
   let bound, ids = Implicit_quantifiers.free_vars_of_binders ~bound [] (sup @ par) in
   let bound = Idset.union bound (Implicit_quantifiers.ids_of_list ids) in
   let sup, bound = name_typeclass_binders bound sup in
+  let par, bound = name_typeclass_binders bound par in
   let supnames = 
     List.fold_left (fun acc b -> 
       match b with