diff options
| author | sacerdot | 2004-09-08 14:08:36 +0000 |
|---|---|---|
| committer | sacerdot | 2004-09-08 14:08:36 +0000 |
| commit | 94139be9382f9a7a03f4abbfe92a68f5d42f67d2 (patch) | |
| tree | f15d8a9600baa4bffd8cce02cc52b0f1a7024982 /dev/include | |
| parent | 2cc7db038d72006bf7d3b418df450c370e447421 (diff) | |
The Coq part of the reflexive tactic is now able to handle also
irreflexive relations (in particular partial setoids, also called
typoids). This feature was asked by Marco Maggesi.
The Coq part of the tactic has now reached the planned expressive power.
However, the ML part does not exploit yet the full expressiveness.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6079 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/include')
0 files changed, 0 insertions, 0 deletions