aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/univops.ml
diff options
context:
space:
mode:
authorGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-07-03 16:25:52 +0000
committerGravatar Vincent Laporte <Vincent.Laporte@gmail.com>2018-07-03 16:25:52 +0000
commit1a4d29ea194833d337ff23320c56e7f324fa82b7 (patch)
tree0e5da8f2df16a904f60b9378d8d1c2d0aa8e1fae /engine/univops.ml
parent1615f76645b0307485ee3143b0d185e91a4935b5 (diff)
fix syntax of .mlg
Diffstat (limited to 'engine/univops.ml')
0 files changed, 0 insertions, 0 deletions