aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-26 14:25:30 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-05-11 13:41:26 +0200
commit81107b12644c78f204d0a46df520b8b2d8e72142 (patch)
tree85b9575ade7ce2dffff6ee66a652706c82b34d2c /pretyping/evarconv.ml
parentc538b7fd555828d9fba9ea97503fac6c70377b76 (diff)
Deprecate Evarconv.e_conv,e_cumul
Diffstat (limited to 'pretyping/evarconv.ml')
0 files changed, 0 insertions, 0 deletions