diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-02 01:51:42 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-03-02 02:04:35 +0100 |
| commit | 4324e5d0f96001607909a4b7d07139192bb46617 (patch) | |
| tree | 088716c90f7b2cdc06f8f7e500dc1522a75f3d4c /stm | |
| 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 'stm')
| -rw-r--r-- | stm/stm.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e7c371798..fd22a8388 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2949,6 +2949,7 @@ let get_ast ~doc id = match VCS.visit id with | { step = `Cmd { cast = { loc; expr } } } | { step = `Fork (({ loc; expr }, _, _, _), _) } + | { step = `Sideff ((ReplayCommand {loc; expr}) , _) } | { step = `Qed ({ qast = { loc; expr } }, _) } -> Some (Loc.tag ?loc expr) | _ -> None |