aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/modules/modulik.v
blob: 50d985e5219f7b335d2a92e1fbbb10c53861261a (plain)
1
2
3
4
5
Definition toto := Set.

Mod M.
  Definition id:=[X:Set]X.
EndM M.