aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/ex/test-cases/change-ancestor/b.v
blob: ddc15cb7f86b3321a4b78b91cb4d1a68c8028759 (plain)
1
2
3
4
5

Require Import a.

Definition b := a.