summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/2846.v
blob: 8d6d348a2eecd4a2ebeb460dd16d397c8c8bb2f8 (plain)
1
2
3
Variable R : Type.

Fail Inductive I : R := c : R.