diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:05:56 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:05:56 +0100 |
| commit | 3f91296b5cf1dc9097d5368c2df5c6f70a04210c (patch) | |
| tree | 372c38b6ced6baadb1edf5b2f27457c05c8467e1 /pretyping | |
| parent | 74c29764359272b29af081b30762549777ae8825 (diff) | |
Remove keys for evar and meta, since they cannot occur.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions