Major speed and space improvements in setoid rewrite:

- Avoid using projections for singleton classes. Divides the size
  of proofs by 2 and simplifies the typechecking as well.
- Switch to the new discrimination net implementation for classes, 
  with the current convention that all constants are unfoldable. 
  Users can add "Typeclasses Opaque" declarations make the dnet 
  discriminate more, otherwise it should be entirely
  backward-compatible.
- Fix bug introduced in r11333 in "transitivity" tactic in presence
  of coercions.
Up to 15% gains on setoid-intensive files like Ring_polynom and
Field_theory. More importantly, performance should not decrease
significantly by adding new Morphism/Setoid declarations.


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

1 files changed, 4 insertions, 3 deletions

diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index 70087b2d4..a0ef16438 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -452,12 +452,13 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
+  let evm = Evd.empty in
   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 |]
+	Class_tactics.reflexive_proof env evm a r ; 
+	Class_tactics.symmetric_proof env evm a r ; 
+	Class_tactics.transitive_proof env evm a r |]
   with Not_found ->
     error "cannot find setoid relation"