Almost fully type-safe implementation of camlp5.

There are still minute uses of type-unsafe primitives. Most of them can be
removed if I had a little higher dan in GADTs (or weeks to spare thinking
about how non-interactive proofs can be performed) but one, which is
really a potential source of unsoundness. The latter is not problematic
as all uses in Coq are protected about the unsoundness proof, but the
API is clearly deficient and needs to be fixed at some point.

0 files changed, 0 insertions, 0 deletions