Merge PR #8955: [ssr] "case/elim: p" don't resolve TC in "p"

3 files changed, 59 insertions, 0 deletions

diff --git a/test-suite/ssr/case_TC.v b/test-suite/ssr/case_TC.v
new file mode 100644
index 0000000000..78ed374432
--- /dev/null
+++ b/test-suite/ssr/case_TC.v
@@ -0,0 +1,18 @@
+From Coq Require Import ssreflect.
+From Coq Require Import ssrbool.
+
+Set Printing All.
+Set Debug Ssreflect.
+
+Class Class := { sort : Type ; op : sort -> bool }.
+Coercion sort : Class >-> Sortclass.
+Arguments op [_] _.
+
+Section Section.
+  Context (A B: Class) (a: A).
+
+  Goal op a || ~~ op a.
+    by case: op.
+  Abort.
+
+End Section.
diff --git a/test-suite/ssr/case_TC2.v b/test-suite/ssr/case_TC2.v
new file mode 100644
index 0000000000..37504d662d
--- /dev/null
+++ b/test-suite/ssr/case_TC2.v
@@ -0,0 +1,20 @@
+From Coq Require Import Bool ssreflect.
+
+Set Printing All.
+Set Debug Ssreflect.
+
+Class Class := { sort : Type ; op : sort -> bool }.
+Coercion sort : Class >-> Sortclass.
+Arguments op [_] _.
+
+Lemma opP (A: Class) (a: A) : reflect True (op a).
+Proof. Admitted.
+
+Section Section.
+  Context (A B: Class) (a: A).
+
+  Goal is_true (op a).
+    by case: opP.
+  Abort.
+
+End Section.
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.