diff options
| author |  Jason Gross <jgross@mit.edu> | 2013-11-21 18:42:43 -0500 |
|---|---|---|
| committer |  Pierre Boutillier <pierre.boutillier@ens-lyon.org> | 2014-04-10 15:05:13 +0200 |
| commit | f705a0b0ae587e323199c43e9669b4f96adf4d77 (patch) | |
| tree | 08af2d10889d5bbe5593a61241d9e3a70d2b150e /theories/Reals/Rseries.v | |
| parent | ff8bac52149f8a32498f765bd579e00fcbd4f080 (diff) | |
Define [projT3] and [proj3_sig]
Also allow [projT1]/[projT2] to work for [sigT2]s and
[proj1_sig]/[proj2_sig] to work for [sig2]s, by means of coercions.
This closes Bug 3044.
This closes Pull Request #4.
Diffstat (limited to 'theories/Reals/Rseries.v')
0 files changed, 0 insertions, 0 deletions