New: (temporary) concrete syntax to specify the morphism signature:

 "Add Morphism m @ arg1 ... argn @ out as ident"

where argi = constr arrow
and arrow =  "-->" | "++>" | "==>" (for contravariant, covariant and
 bi-variant morphisms).

The syntax should be improved by getting rid of the "@" and maybe choosing
better symbols to represent the arrows.


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

0 files changed, 0 insertions, 0 deletions