aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/cctac.ml
diff options
context:
space:
mode:
authorGravatar amblaf <you@example.com>2017-06-20 09:43:11 +0200
committerGravatar amblaf <you@example.com>2017-07-31 10:34:05 +0200
commit5c7d5fce3ed1de62ff5e1528a12adce0cdf2b0d9 (patch)
tree0226e3c89d314b79d2dcc4e4a10e10e7b5d0eeea /plugins/cc/cctac.ml
parent7a56397ae26854df6335a3325353d0a5d6c894ea (diff)
env, sigma as first arguments of functions
Diffstat (limited to 'plugins/cc/cctac.ml')
0 files changed, 0 insertions, 0 deletions