diff options
| author | Guillaume Melquiond | 2015-07-30 10:19:35 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-07-30 10:19:35 +0200 |
| commit | 5cf7ce6afae0e8e5310755f05a26450f428da04f (patch) | |
| tree | d716bedacdf8234ca07bcf3f3830ec00328fbe56 /kernel/nativecode.mli | |
| parent | 8ccd08f6bc6bcbda01cf65d2b6e7ecd62e4c4972 (diff) | |
Avoid suggesting elim and decompose in the FAQ.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions