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

0 files changed, 0 insertions, 0 deletions