From a8d50dd372fc9365d3f6f21551567f05937d93ef Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 5 Jan 2008 19:10:06 +0000
Subject: Fix a naming bug reported by Arnaud Spiwack, allow instance search to
 create evars and try to solve them too. Finally, rework tactics on setoids
 and design a saturating tactic to help solve goals on any setoid.

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

(limited to 'interp/implicit_quantifiers.ml')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index c029550a13..4799eb7b39 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -99,7 +99,7 @@ let combine_params avoid applied needed =
     match app, need with
 	[], need -> 
 	  let need', avoid = ids_of_named_context_avoiding avoid (List.map snd need) in
-	    List.rev ids @ (List.map mkIdentC need'), avoid
+	    List.rev ids @ (List.rev_map mkIdentC need'), avoid
       | _, (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
@@ -130,7 +130,9 @@ let full_class_binders env l =
 	      (try
 		  let c = class_info (snd id) 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) 
+		    (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)
-- 
cgit v1.2.3