diff options
| author | Nadrieril | 2019-04-23 17:16:29 +0200 |
|---|---|---|
| committer | Nadrieril | 2019-04-23 17:16:29 +0200 |
| commit | a97ebd37169193c6392658aa8b022c7e0f8c4a34 (patch) | |
| tree | 8764f6375d2164e061e0f1b7f04e27a6537b7ab1 /.gitignore | |
| parent | 2f1fa26abd9c9f2b75d24b18877d3b278f7d2a01 (diff) | |
Avoid constructing ExprF::Pi while typechecking
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions