Fix hashconsing of terms in the kernel.

In one case, the hashconsed type of a judgement was not used anywhere else.

In another case, the Opaqueproof module was rehashconsing terms that had
already gone through a hashconsing phase. Indeed, most OpaqueDef constructor
applications actually called it beforehand, so that the one performed in
Opaqueproof was most often useless. The only case where this was not true
was at section closing time, so that we tweak the Cooking.cook_constant to
perform hashconsing for us.

0 files changed, 0 insertions, 0 deletions