diff options
| author | Emilio Jesus Gallego Arias | 2018-03-02 01:51:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-03-02 02:04:35 +0100 |
| commit | 4324e5d0f96001607909a4b7d07139192bb46617 (patch) | |
| tree | 088716c90f7b2cdc06f8f7e500dc1522a75f3d4c /kernel/nativecode.mli | |
| parent | f726e860917b56abc94f21d9d5add7594d23bb6d (diff) | |
[stm] Partial fix for bug #6884 [location missing from replay nodes]
Example not yet fixed by this patch:
```
Definition u : Type.
Definition m : Type.
exact nat.
Defined.
exact bool.
Defined.
```
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions