Fix the checker by merely adapting the data structure.

Unluckily, this is completely wrong as we trust the inlined term to be
well-typed in some unavailable environment. To start with, the checker
should not even rely on substitutions as it does not trust functors,
but it does anyways. I have thus commented this code as a useful backdoor
for when Coq is used to implement the next blockchain Ponzi scheme.

We really need to sort this out though.

0 files changed, 0 insertions, 0 deletions