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

1 files changed, 8 insertions, 5 deletions

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 |]