Enhanced discrimination nets implementation, which can now work with

goals containing existentials and use transparency information on
constants (optionally). Only used by the typeclasses eauto engine for
now, but could be used for other hint bases easily (just switch a boolean).
Had to add a new "creation" hint to be able to set said boolean upon
creation of the typeclass_instances hint db.
Improve the proof-search algorithm for Morphism, up to 10 seconds
gained in e.g. Field_theory, Ring_polynom. Added a morphism
declaration for [compose].
One needs to declare more constants as being unfoldable using
the [Typeclasses unfold] command so that discrimination is done correctly, but
that amounts to only 6 declarations in the standard library.


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

4 files changed, 26 insertions, 21 deletions

diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml
index e540058f14..fd5972fb74 100644
--- a/contrib/firstorder/sequent.ml
+++ b/contrib/firstorder/sequent.ml
@@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl=
 	searchtable_map dbname
       with Not_found-> 
 	error ("Firstorder: "^dbname^" : No such Hint database") in
-      Hint_db.iter g (snd hdb) in
+      Hint_db.iter g hdb in
     List.iter h l;
     !seqref
 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 3d80bd0040..d7bcde69cb 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				      false
 				      (true,5)
 				      [Lazy.force refl_equal]
-				      [empty_transparent_state, Auto.Hint_db.empty]
+				      [Auto.Hint_db.empty false]
 				  )
 			   )
 			)
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 6ec0fac42d..767a7dd667 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	     (add_hint_list hintl local_db) g'))) ::
+	     (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
-  let flags = Auto.auto_unif_flags in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) 
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
@@ -279,7 +280,7 @@ module MySearchProblem = struct
 	     let hintl = 
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-             let ldb = add_hint_list hintl (List.hd s.localdb) in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl =
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
-  let flags = Auto.auto_unif_flags in
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) 
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   List.map 
     (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
@@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
 	  g'))
   in
   let rec_tacs = 
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 474b3616a8..70087b2d44 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
-  lapp coq_mk_Setoid
-    [|a ; r ; 
-      Class_tactics.reflexive_proof env a r ; 
-      Class_tactics.symmetric_proof env a r ; 
-      Class_tactics.transitive_proof env a r |]
+  try 
+    lapp coq_mk_Setoid
+      [|a ; r ; 
+	Class_tactics.reflexive_proof env a r ; 
+	Class_tactics.symmetric_proof env a r ; 
+	Class_tactics.transitive_proof env a r |]
+  with Not_found ->
+    error "cannot find setoid relation"
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]