aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:03 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2016-04-27 22:13:03 +0200
commit2c72ba5cb6864936067dd23cc40e28fe82f14ec5 (patch)
tree004f07a6f330eebed1bef01d8e26022ce522b406 /pretyping/coercion.ml
parenta89f5a422d565c52e0c536d7aca2b93f5052f248 (diff)
Revert "Fixing printing of Function."
Diffstat (limited to 'pretyping/coercion.ml')
0 files changed, 0 insertions, 0 deletions