Testing {in _, _} and {pred _} from ssrbool

(cherry picked from commit 36664ba)
coq · Dec 9, 2020 · 831c47d · 831c47d
1 parent ef1f5bb
commit 831c47d
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 0 deletions.
diff --git a/test-suite/output/ssr_pred.out b/test-suite/output/ssr_pred.out
@@ -0,0 +1,3 @@
+in1W
+     : forall (T1 : predArgType) (D1 : {pred T1}) (P1 : T1 -> Prop),
+       (forall x : T1, P1 x) -> {in D1, forall x : T1, P1 x}
diff --git a/test-suite/output/ssr_pred.v b/test-suite/output/ssr_pred.v
@@ -0,0 +1,3 @@
+Require Import ssreflect ssrfun ssrbool.
+
+Check @in1W.