2388.v « shouldsucceed « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/shouldsucceed/2388.v

blob: 8cc43ee6baa1ccbb3bdf20b3038402393d8c42e8 (plain)

(* Error message was not printed in the correct environment *)

Fail Parameters (A:Prop) (a:A A).