aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-29 17:49:11 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:30:44 +0100
commit390fd4ac0a969103caeb5db3e5138e26f9a533de (patch)
treef04f87b0fca81518797dabd0f9d2d395ba8ec2b8 /engine/termops.mli
parentd549d9d3d169fbfc5f555e3e4f22f46301161d53 (diff)
Chasing a few unsafe constr coercions.
Diffstat (limited to 'engine/termops.mli')
0 files changed, 0 insertions, 0 deletions