3337.v « opened « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

path: root/test-suite/bugs/opened/3337.v

blob: 06acd020a98fc7ae34f625325f0d41564be6c637 (plain)

Require Import Setoid.
Goal forall x y : Set, x = y -> x = y.
intros x y H.
Fail rewrite_strat subterms H.