From 4324e5d0f96001607909a4b7d07139192bb46617 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 2 Mar 2018 01:51:42 +0100
Subject: [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.
```
---
 stm/stm.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'stm')

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
-- 
cgit v1.2.3