diff options
| author | sacerdot | 2004-10-15 13:10:39 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-15 13:10:39 +0000 |
| commit | 32e3ed47b676960383d53961492374526189161d (patch) | |
| tree | 8f338ddafb9d250db6ff5595650368af56f05b3b /kernel/cbytecodes.ml | |
| parent | a6554e3b8fb6a9e7081cf864f205cdb057c4c8f5 (diff) | |
Wish of Maggesi implemented: the type of the morphism compatibility lemma
is now the one that is shown to the user (and not only convertible to it).
In this way it is possible to register the lemma in the Hint database.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions