1. added new parameter "as ..." to Add Setoid. Used to synthesize the name

   of the morphism. Previously the name was automatically generated, but it
   was impossible to generate the same name in a module type and in a module.
2. behaviour of the relation/morphism tables w.r.t. module types and functors
   fixed.
3. relations/setoids/morphisms can now happear in a module type. Add Morphism
   in a module type declares an axiom instead of starting a new proof.
   Add Morphism/Add Relation/Add Setoid in a module now generate objects
   that match those generated by the same commands in a module type.
4. error messages improved/fixed.


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

0 files changed, 0 insertions, 0 deletions