aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-05-31 15:06:46 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2014-05-31 19:10:08 +0200
commitbe01deca2b8ff22505adaa66f55f005673bf2d85 (patch)
treec0853a41fc88a860f5a835072934aba8a8e1feeb /theories/Reals
parent37f68259ab0a33c3b5b41de70b08422d9bcd3bec (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