* Code simplification and clean-up. In particular there is no more code

  duplicated between add_relation and add_setoid.
* Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v
* Term size reduction (first part): when a relation is registered, we add
  to the environment a definition that gives back either the relation as
  an argument or as a relation class. The definition is used to reduce
  the term size. [ Note: we could save a bit more by defining two definitions
  in place of one. However, we suppose that the lambda term fragments generated
  can be shared quite effectively. Thus we would recive almost no benefit by
  sharing in terms of size. What about proof checking time? ]


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

0 files changed, 0 insertions, 0 deletions