diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:59:45 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-08-10 11:59:45 +0200 |
| commit | 5f7463e1ad99f530e078ecbc600347328d603bb4 (patch) | |
| tree | c5bfca90c4639047d0d14d5efa7c350a4bdc6dd5 /pretyping | |
| parent | 90303e38d22479105927f0dd2fe95cce9447bd44 (diff) | |
Make code a bit clearer by removing optional argument.
Diffstat (limited to 'pretyping')
0 files changed, 0 insertions, 0 deletions