diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-04-14 20:28:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-04 13:47:12 +0200 |
| commit | d2f0db714bd2d393423cf2dcb4ed37913029e052 (patch) | |
| tree | 076830d28c09be47fae9235b50f7c33cd65af101 /lib/genarg.mli | |
| parent | 8ad2627de29639b21473783195905dca6bb1c6ae (diff) | |
Simplifying the code of Tacinterp.
Diffstat (limited to 'lib/genarg.mli')
0 files changed, 0 insertions, 0 deletions