blob: 114bf2cecf790aaf7b2ff9cc3f12848cd1b45a1b (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
From Coq Require Import ssreflect.
Axiom T : Type.
Axiom R : T -> T -> Type.
(** Check that internal exceptions are correctly caught in the monad *)
Goal forall (a b : T) (Hab : R a b), True.
Proof.
intros.
try (case: Hab).
Abort.
|
