ssr: add another test for elim + TC

1 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/ssr/case_TC3.v b/test-suite/ssr/case_TC3.v
new file mode 100644
index 0000000000..92e166e85d
--- /dev/null
+++ b/test-suite/ssr/case_TC3.v
@@ -0,0 +1,21 @@
+From Coq Require Import Utf8 Bool ssreflect.
+
+Set Printing All.
+Set Debug Ssreflect.
+
+Class Class sort := { op : sort → bool }.
+Arguments op {_ _}.
+Hint Mode Class !.
+
+Lemma opP A (C: Class A) (a: A) : reflect True (op a).
+Proof. Admitted.
+Arguments op {_ _}.
+
+Section Section.
+  Context A B (CA : Class A) (CB : Class B) (a: A).
+
+  Goal is_true (op a).
+    by case: opP.
+  Abort.
+
+End Section.