aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/states.mli
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-12 16:39:32 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 15:05:04 +0100
commit5f2f22e7ff5d53e3258affa0e0e41666d5e0691d (patch)
treea8a52df78e46d9b663f5583f36aa1afe401fdd05 /library/states.mli
parenteb1eddf24932232890e32acf0fc4ff418ad0c281 (diff)
Global: export the name of the summary entry
In this way one can make surgery on the system states, like checking if two frozen states have the same environment (i.e. no running "abstract" in between)
Diffstat (limited to 'library/states.mli')
0 files changed, 0 insertions, 0 deletions