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.
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: 44dc50bdcc0f5d1a212c497508dc9452e0b35e2b@6171 85f007b7-540e-0410-9357-904b9bb8a0f7

ejgallego/coq,gmalecha/coq,8l/coq,ppedrot/coq,tomprince/coq,Matafou/coq,maximedenes/coq,Lionel-Rieg/coq,Lionel-Rieg/coq,gares/coq,jpdeplaix/coq,amintimany/coq,TOSPIO/coq,JasonGross/coq,william-lawvere/coq,letouzey/coq-wip,herbelin/github-coq,herbelin/github-coq,silene/coq,JasonGross/coq,mlasson/coq,jpdeplaix/coq,mattam82/coq,Matafou/coq,mattam82/coq,pirapira/coq2rust,pirbo/coq,coq/coq,coq/coq,maximedenes/coq,SkySkimmer/coq,Zimmi48/coq,gmalecha/coq,asr/coq,Lionel-Rieg/coq,jhjourdan/coq,gares/coq,jhjourdan/coq,pirapira/coq2rust,mattam82/Coq-misc,barras/coq,ppedrot/coq,amintimany/coq,amintimany/coq,letouzey/coq-wip,herbelin/coq-hh,SkySkimmer/coq,aspiwack/coq,Zimmi48/coq,8l/coq,gmalecha/coq,barras/coq,maximedenes/coq,Ptival/coq,SkySkimmer/coq,asr/coq,TOSPIO/coq,ale-f/coq,8l/coq,coq/coq,Ptival/coq,TOSPIO/coq,Zimmi48/coq,mattam82/Coq-misc,mattam82/coq,ppedrot/coq,ppedrot/coq,shindere/coq,pirbo/coq,shindere/coq,ppedrot/coq,TheTypoMaster/coq,SkySkimmer/coq,william-lawvere/coq,ale-f/coq,jpdeplaix/coq,herbelin/coq-hh,maximedenes/coq,TheTypoMaster/coq,gares/coq,tomprince/coq,letouzey/coq-wip,JasonGross/coq,ejgallego/coq,ejgallego/coq,asr/coq,Ptival/coq,Matafou/coq,aspiwack/coq,william-lawvere/coq,shindere/coq,mlasson/coq,letouzey/coq-wip,pirapira/coq2rust,silene/coq,barras/coq,aspiwack/coq,letouzey/coq-wip,coq/coq,jhjourdan/coq,herbelin/github-coq,tomprince/coq,maximedenes/coq,mlasson/coq,ejgallego/coq,TheTypoMaster/coq,pirbo/coq,gares/coq,ale-f/coq,Zimmi48/coq,gares/coq,silene/coq,JasonGross/coq