diff options
| author | Maxime Dénès | 2018-03-04 16:44:29 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-03-04 16:44:29 +0100 |
| commit | d28726426b048c9c4d521774f6540596a33165c4 (patch) | |
| tree | b74dc3632626d06c96fe38be4e2f1ff249c2db35 | |
| parent | 6b6cf6113dbeeb0edfd206589da1285631d22fb8 (diff) | |
| parent | 4324e5d0f96001607909a4b7d07139192bb46617 (diff) | |
Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from replay nodes]
| -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 e7c3717988..fd22a83886 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 |