diff options
| author | Daniel R. Grayson | 2015-01-26 20:56:45 -0600 |
|---|---|---|
| committer | Hugo Herbelin | 2015-01-27 14:05:01 +0100 |
| commit | 73ac958a49e54f2bedcac7f8557537e0bf524068 (patch) | |
| tree | 118a6fc007e560cb78c00c5b3915e949c4d9c331 /kernel | |
| parent | 96fb5028a131627f5348bbec315f3b1223837e7b (diff) | |
Allow -type-in-type to be an option also for coqc.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions