aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/coercion.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-02 16:30:54 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-05-02 16:30:54 +0200
commit4bff930da2c029a66eaf5378e5abd2cc35554f8f (patch)
tree6c0a89614fd65c681a0f5c3105f7aa11914327c3 /pretyping/coercion.ml
parent28accc370aa2f6fafbf50b69be7ae5dc06104212 (diff)
parent5c7163d2ee1412fa5af523fbcd275518fc61fbde (diff)
Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.
Diffstat (limited to 'pretyping/coercion.ml')
0 files changed, 0 insertions, 0 deletions