diff options
| author | Hugo Herbelin | 2014-05-31 15:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-05-31 19:10:08 +0200 |
| commit | be01deca2b8ff22505adaa66f55f005673bf2d85 (patch) | |
| tree | c0853a41fc88a860f5a835072934aba8a8e1feeb /pretyping | |
| parent | 37f68259ab0a33c3b5b41de70b08422d9bcd3bec (diff) | |
More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions