ssrmatching: unify_HO does not resolve type classes

2 files changed, 38 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.