aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/spawned.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-09-30 22:18:56 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-10-08 09:51:13 +0200
commitf7e9e6428842dd80549a0dcd20bf872c2dd7fa8c (patch)
tree1065eccd48e1c291faec73dcf75ee9777adfcab5 /stm/spawned.ml
parent173f07a8386bf4d3d45b49d3dc01ab047b3ad4f9 (diff)
STM: for PIDE based UIs, edit_at requires no Reach.known_state
Diffstat (limited to 'stm/spawned.ml')
0 files changed, 0 insertions, 0 deletions