diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-06 18:54:05 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-06 18:54:05 +0000 |
| commit | 9af983945cb1f2b7bcee95cab3ca55927b614b38 (patch) | |
| tree | af62e432788714941ca6eba9a05d851ad4a80422 /theories/Setoids/.cvsignore | |
| parent | c29aa4ce8fe8090ca1a84d0be020e40787149c38 (diff) | |
* New syntactic sugar: Add Relation ... transitivity proved by ...
now declares both the relation and the relation as a morphism, computing
the appropriate signature (depending on the reflexivity of the relation).
* New parameter "as ..." to Add Relation (to be able to compute the
morphism name).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6189 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Setoids/.cvsignore')
0 files changed, 0 insertions, 0 deletions