ssr_delayed_clear_rename.v « success « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/success/ssr_delayed_clear_rename.v

blob: 951e5aff795991f6f581f9a5a1ebcff240e7f109 (plain)

Require Import ssreflect.
Example foo (t t1 t2 : True) : True /\ True -> True -> True.
Proof.
move=>[{t1 t2 t} t1 t2] t.
Abort.