From fb825197d08554a208437ee31755a783ce48708b Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 19 Jun 2018 13:54:05 +0200 Subject: [ssr] test case for rewrite (setoid) making the goal illtyped --- test-suite/ssr/ssr_rew_illtyped.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/ssr/ssr_rew_illtyped.v (limited to 'test-suite/ssr') diff --git a/test-suite/ssr/ssr_rew_illtyped.v b/test-suite/ssr/ssr_rew_illtyped.v new file mode 100644 index 000000000..7358068c8 --- /dev/null +++ b/test-suite/ssr/ssr_rew_illtyped.v @@ -0,0 +1,9 @@ +From Coq Require Import ssreflect Setoid. + +Structure SEProp := {prop_of : Prop; _ : prop_of <-> True}. + +Fact anomaly: forall P : SEProp, prop_of P. +Proof. +move=> [P E]. +Fail rewrite E. +Abort. -- cgit v1.2.3