From 0d2594da361eb939a14e4917852389a19e1e2ba0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 13 Nov 2018 21:56:43 +0100
Subject: ssr: add another test for elim + TC

---
 test-suite/ssr/case_TC3.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 test-suite/ssr/case_TC3.v

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.
-- 
cgit v1.2.3