diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-31 15:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-31 19:10:08 +0200 |
| commit | be01deca2b8ff22505adaa66f55f005673bf2d85 (patch) | |
| tree | c0853a41fc88a860f5a835072934aba8a8e1feeb /theories/Reals | |
| 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 'theories/Reals')
0 files changed, 0 insertions, 0 deletions