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

summary refs log tree commit diff

path: root/test-suite/bugs/closed/shouldfail/2586.v

blob: 6111a6415f1cffdf4e31647fe347c01904d2806a (plain)

Require Import Setoid SetoidClass Program.

Goal forall `(Setoid nat) x y, x == y -> S x == S y.
  intros.
  clsubst H0.