diff options
| author | Gaëtan Gilbert | 2018-06-23 15:08:55 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 12:03:10 +0200 |
| commit | 7817af48a554573fb649028263ecfc0fabe400d8 (patch) | |
| tree | 1298a503c997f8246fe726142f4fa8b2121c97e8 /dev/vm_printers.ml | |
| parent | fb9003c7850c459d7a5981212d8ef87de877bd9f (diff) | |
Remove useless is_projection in tacred
Diffstat (limited to 'dev/vm_printers.ml')
0 files changed, 0 insertions, 0 deletions