diff options
| author | Maxime Dénès | 2018-10-30 12:00:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-30 13:10:02 +0100 |
| commit | 365f14bdb87f6f323d635267f69f507b540ef2a8 (patch) | |
| tree | a3b29564bf17adebc44fc31ab23f99012cdcc88b /pretyping | |
| parent | 000bf6684a872bc29191807c29a64011f7f82350 (diff) | |
Remove one use of empty_env in ssr
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions