diff options
| author | sacerdot | 2004-10-01 16:33:00 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-01 16:33:00 +0000 |
| commit | 4eafa8d4cc44da82f528cf61508330a6a28355b2 (patch) | |
| tree | 29372c79b77898304fcbceca55c637e5c34fc070 /dev/Makefile.subdir | |
| parent | 0d34c71a1a02c5e2d1718b039a8da484a22cc068 (diff) | |
The "Add Setoid" command now has a new argument "as name" that is used
to generate the name of the morphism. Previously the name was automatically
generated, but this behaviour was not compatible with module typing: it
was not possible to generate the same identifier in the module type and in
the module.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6168 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/Makefile.subdir')
0 files changed, 0 insertions, 0 deletions