index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
test-suite
/
coqchk
/
bug_8655.v
blob: 06d08b2082f617f75e6c48d15cca5e4915f39df1 (
plain
)
1
Inductive IND2 (A:Type) (T:=fun _ : Type->Type => A) := CONS2 : IND2 A -> IND2 (T IND2).
