aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
diff options
context:
space:
mode:
authorJason Gross2017-02-21 20:43:46 -0500
committerJason Gross2017-05-28 09:38:36 -0400
commit4e12d9eb8945120c5cfdb36964fba54dde767b51 (patch)
treec7fc5c13f6c8a981974e9257f0f4cbd27e102266 /dev/base_include
parent6d3c5956ee7c56c816750f3879a5ddafcdf81f0f (diff)
Replace [ex'] with [ex]
The ' was originally denoting that we were taking in the projections and applying the constructor in the conclusion, rather than taking in the bundled versions and projecting them out (because the projections don't exist for [ex] and [ex2]). But we don't have versions like this for [sig] and [sigT] and [sigT2] and [sig2], so we might as well not add the ' to the [ex] and [ex2] versions.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions