Stop using the discrimination net in typeclasses/setoid rewrite, which was

considering every definition opaque by default, until a better fix is
found.


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

1 files changed, 17 insertions, 14 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 68cf37b49e..6312cefc18 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -43,7 +43,7 @@ open Evd
 let default_eauto_depth = 100
 let typeclasses_db = "typeclass_instances"
 
-let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db true)
+let _ = Auto.auto_init := (fun () -> Auto.create_hint_db false typeclasses_db false)
 
 let check_imported_library d =
   let d' = List.map id_of_string d in
@@ -108,13 +108,13 @@ let rec e_trivial_fail_db db_list local_db goal =
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
   let hintl =
-(*     if occur_existential concl then *)
-(*       list_map_append *)
-(* 	(fun db -> *)
-(* 	  let st = Hint_db.transparent_state db in *)
-(* 	    List.map (fun x -> (st, x)) (Hint_db.map_all hdc db)) *)
-(* 	(local_db::db_list) *)
-(*     else *)
+    if occur_existential concl then
+      list_map_append
+	(fun db ->
+	  let st = Hint_db.transparent_state db in
+	    List.map (fun x -> (st, x)) (Hint_db.map_all hdc db))
+	(local_db::db_list)
+    else
       list_map_append
 	(fun db -> 
 	  let st = Hint_db.transparent_state db in
@@ -201,12 +201,15 @@ module SearchProblem = struct
 (* 	    if !debug then msg (str"\nTrying tactic: " ++ pptac ++ str"\n"); *)
 	    let (lgls,ptl) = apply_tac_list tac glls in 
 	    let v' p = v (ptl p) in
-(* 	      	      if !debug then *)
-(* 	      		begin *)
-(* 	      		  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
-(* 	      		    msg (str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n"); *)
-(* 	      		    msg (hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n")) *)
-(* 	      		end; *)
+(* 	      if !debug then *)
+(* 	      	begin *)
+(* 	      	  let evars = Evarutil.nf_evars (Refiner.project glls) in *)
+(* 	      	  let pptac = str"\nOn goal: " ++ pr_ev evars (List.hd (sig_it glls)) ++ str"\n" *)
+(* 		    ++ hov 1 (pptac ++ str" gives: \n" ++ pr_goals lgls ++ str"\n") *)
+(* 		  in *)
+(* 		    ((lgls,v'),pri,pptac) :: aux tacl *)
+(* 	      	end *)
+(* 	      else *)
 	      ((lgls,v'),pri,pptac) :: aux tacl
 	  with e when catchable e -> aux tacl
     in aux l