diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-09 16:43:04 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-09 16:43:04 +0000 |
| commit | 67021c6861020d5b0969a6c5856304e2486fb56d (patch) | |
| tree | 6dc8d87fb02f568e576e8398adb2b5950030a03d /pretyping/pretyping.ml | |
| parent | 85af5bb1ec5b2f080e267b8a8bb4438f8f640eb1 (diff) | |
Add a missing morphism declaration that turns morphisms on R ==> R' to
morphisms on R --> inverse R' for any R, R' (report by N. Tabareau).
Better implementation of unfolding for impl that does it only where
necessary to keep the goal in the same shape as the user gave.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10648 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretyping.ml')
0 files changed, 0 insertions, 0 deletions