diff options
| author | Frédéric Besson | 2014-08-01 18:42:26 +0200 |
|---|---|---|
| committer | Frédéric Besson | 2014-08-01 18:42:26 +0200 |
| commit | fb50696d492027744c3c9044fd863f93e0a1605c (patch) | |
| tree | 69003e4485d5a3f7cbebffc54328ac3f0a2426c5 /kernel/nativecode.mli | |
| parent | a8d440fcb2a5f5768874012e72c3e092eb82eff1 (diff) | |
micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)
* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions