Make explicit the delayed computation of opaque bodies in Term_typing.

We separate the Term_typing inference API into two functions, one to
typecheck just the immediate part of an entry, and another one to check
after the fact that a delayed term is indeed a correct proof for an opaque
entry.

This commit is mostly moving code around, this should be 1:1 semantically.

0 files changed, 0 insertions, 0 deletions