Better resolution of implicit parameters in typeclass binders, add extensionality tactic to apply the axiom properly and fix test-suite.

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

1 files changed, 10 insertions, 5 deletions

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7be0b015e..2de7945ee 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -92,14 +92,17 @@ let ids_of_named_context_avoiding avoid l =
     ([], avoid) (Termops.ids_of_named_context l)
     
 let combine_params avoid applied needed =
-  let rec aux ids app need =
+  let rec aux ids avoid app need =
     match app, need with
 	[], need -> 
-	  let need', avoid = ids_of_named_context_avoiding avoid need in
+	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
 	    List.rev ids @ (List.map mkIdentC need'), avoid
-      | x :: app, _ :: need -> aux (x :: ids) app need    
+      | _, (true, (id, _, _)) :: need -> 
+	  let id' = next_ident_away_from id avoid in
+	    aux (CRef (Ident (dummy_loc, id')) :: ids) (Idset.add id' avoid) app need
+      | x :: app, (false, _) :: need -> aux (x :: ids) avoid app need    
       | _ :: _, [] -> failwith "combine_params: overly applied typeclass"
-  in aux [] applied needed
+  in aux [] avoid applied needed
 
 let compute_context_vars env l =
   List.fold_left (fun avoid (iid, _, c) -> 
@@ -123,7 +126,9 @@ let full_class_binders env l =
 	    let (id, l) = destClassApp cl in
 	      (try
 		  let c = class_info (snd id) in
-		  let args, avoid = combine_params avoid l (List.rev c.cl_context @ List.rev c.cl_super @ List.rev c.cl_params) in
+		  let args, avoid = combine_params avoid l 
+		    (List.rev_map (fun x -> false, x) c.cl_context @ List.rev_map (fun x -> true, x) c.cl_super @ List.rev_map (fun x -> false, x) c.cl_params) 
+		  in
 		    (iid, bk, CAppExpl (fst id, (None, Ident id), args)) :: l', avoid
 		with Not_found -> unbound_class (Global.env ()) id)
 	| Implicit -> (x :: l', avoid))