diff options
| author | sacerdot | 2004-09-08 14:10:07 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-08 14:10:07 +0000 |
| commit | 5931c481426ab253473c7539656c0f6bb50c662c (patch) | |
| tree | 451ea30d695be344fc67f237b38ac3969dc04c2c /dev/include | |
| parent | 94139be9382f9a7a03f4abbfe92a68f5d42f67d2 (diff) | |
The Coq part of the reflexive part can now deal with irreflexive relations too.
In particular it can deal with partial setoids (also called typoids).
The latter feature was request by Marco Maggesi.
This commit is just a porting of the ML part of the tactic to the new
Coq part. It does not allow to exploit the new potentialities, yet.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6080 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions