Type-checking PTS
Coq sources
.
Slides of the talk given at the TYPES'96 Workshop,
postscript
version.