test-suite/bugs/closed/bug_3944.v


1
2
3
4
5
6

Require Import Setoid.
Definition C (T : Type) := T.
Goal forall T (i : C T) (v : T), True.
Proof.
Fail setoid_rewrite plus_n_Sm.
Abort.