From 6f8a4cd773166c65ab424443042e20d86a8c0b33 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 22 Oct 2008 18:44:59 +0000
Subject: Fix bugs #1975 and #1976.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11494 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/implicit_quantifiers.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index f726f8992e..4daf219551 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
 
-- 
cgit v1.2.3