3944.v « closed « bugs « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/bugs/closed/3944.v

blob: 58e60f4f2e363f6ab88423b2527935f17258083e (plain)

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