DecidableType2+OrderedType2 : notations in specific Module Type, slicing of OrderedType2

 OrderedType2 is reorganized in atomic module type following the same approach used
 for DecidableType2.

 We use the following convention: module type Foo' is exactly module type Foo,
 except that some notations may have been added. In functor arg, we can use
 Foo or Foo' depending on whether we want nice notation or not. Note that any
 implementation of Foo is accepted as implementation of Foo' :-). For the moment,
 these notations are not placed in specific scopes, I think it isn't useful, but
 I may be wrong, we'll see later when using them.

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

0 files changed, 0 insertions, 0 deletions