aboutsummaryrefslogtreecommitdiff
path: root/kernel/uGraph.mli
diff options
context:
space:
mode:
authorHugo Herbelin2020-05-02 23:22:48 +0200
committerHugo Herbelin2020-05-06 17:04:11 +0200
commit20f0e2efb87541e511cf31e220a44e4376c44550 (patch)
treeb08810a8fb0d6ac422b88e49f37a06ffd4dce550 /kernel/uGraph.mli
parent86cdd51c4e25fceb12854863419fbdc3f19e44aa (diff)
Moving lazymatch and multimatch to simple identifiers.
Diffstat (limited to 'kernel/uGraph.mli')
0 files changed, 0 insertions, 0 deletions