2ae809c971
Idents.enter_node should be called when entering a node, it is done automagically by the mapfold unless you call directly Hept_mapfold.node_dec. |
||
---|---|---|
.. | ||
global | ||
_tags | ||
graph.ml | ||
misc.ml | ||
misc.mli | ||
pp_tools.ml | ||
pp_tools.mli |