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

summary refs log tree commit diff

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

blob: 7f33afcc2f1f55a13c27a930a7d750c1152bb46e (plain)

From Coq Require Import ssreflect.

Lemma normalizeP (p : tt = tt) : p = p.
Proof.
Fail move: {2} tt p.
Abort.