(* Nicer error messages. Instead of being asked to prove `False`, you are asked to prove `error (hopefully useful message)`. *) Module Type error_spec. Parameter error : forall {T : Type}, T -> Prop. Axiom error_elim : forall {msgType} {msg : msgType} {T}, error msg -> T. End error_spec. Module Export error : error_spec. Definition error {T} (msg : T) := False. Definition error_elim {msgType} (msg : msgType) T : error msg -> T := False_rect T. End error.