bug_5764.v « closed « bugs « test-suite - coq - The formal proof system

about summary refs log tree commit diff

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

blob: 0b015d9c7e5af008c860cefec499e19d5a86e6dd (plain)

Module Type A.
Parameter a : nat.
End A.

Module B (mA : A).
Ltac cbv_a := cbv [mA.a].
End B.