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 /pretyping/pretyping.ml | |
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 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions