diff options
| author | sacerdot | 2004-10-18 14:53:30 +0000 |
|---|---|---|
| committer | sacerdot | 2004-10-18 14:53:30 +0000 |
| commit | 3c76f306c68a0ea4f02700043c4b4b1be877f4e9 (patch) | |
| tree | 43e14323f2ecf6e0a047f42d25f730fed5444512 /kernel/cbytecodes.ml | |
| parent | 5da0ac62b272c7595da16222e8e9004dc4d459a9 (diff) | |
The "lem" field of a morphism used to be the compatibility proof, but it
became the whole structure of type Morphism_Theory. A new field morphism_theory
has now been added to record both informations. Print Setoids now prints again
the right information.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6235 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions