diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 14:44:57 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 14:44:57 +0000 |
| commit | 11104cdcb1e53cd83768d2ce9858829b457e2d65 (patch) | |
| tree | e58d2a0109b7ad010d80c3152780f1877485b2a8 /proofs/clenvtac.mli | |
| parent | 3582bc9ebb612f9541ef02c95af0e2191b83cf58 (diff) | |
* The Coq part of the reflexive tactic setoid_rewrite is generalized to
asymmetric relations thanks to the introduction of morphisms that are
covariant or contravariant in their arguments.
* The ML part of the tactic is updated only for backward compatibility: it
is still not possible to benefit from the asymmetric relations and relative
morphisms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6070 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenvtac.mli')
0 files changed, 0 insertions, 0 deletions