diff options
| author | Matthieu Sozeau | 2014-10-07 15:17:58 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-07 15:19:45 +0200 |
| commit | 8b257187f9b7ec95017a2df14b49c057d254ad15 (patch) | |
| tree | fe770868ede02aedfdd466eacb5296b2657f4c1e /dev | |
| parent | ef7b099bb91ac53770aab886a2051e0c1a1cd056 (diff) | |
Build unfolded versions of the primitive projection in let (a, p) := ...
to maintain compatibility (HoTT bug #557).
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions