diff options
| author | Jason Gross | 2017-02-21 20:43:46 -0500 |
|---|---|---|
| committer | Jason Gross | 2017-05-28 09:38:36 -0400 |
| commit | 4e12d9eb8945120c5cfdb36964fba54dde767b51 (patch) | |
| tree | c7fc5c13f6c8a981974e9257f0f4cbd27e102266 /API/API.ml | |
| parent | 6d3c5956ee7c56c816750f3879a5ddafcdf81f0f (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 'API/API.ml')
0 files changed, 0 insertions, 0 deletions
