diff options
| author | Pierre-Marie Pédrot | 2016-05-09 19:12:24 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-10 19:28:24 +0200 |
| commit | 53724bbcce87da0b1a9a71da4e5334d7a893ba49 (patch) | |
| tree | 64eaefd8051cd92cb7bed27540dc98aa13887dcf /kernel/nativecode.ml | |
| parent | 6150d15647afc739329019f7e9de595187ecc282 (diff) | |
Purer implementation of empty level registering in Pcoq.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions