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.

1 files changed, 4 insertions, 1 deletions

diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f147ea343..74ba73508 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -48,7 +48,10 @@ let turn_indirect dp o (prfs,odp) = match o with
       then CErrors.anomaly (Pp.str "Indirect in a different table")
       else CErrors.anomaly (Pp.str "Already an indirect opaque")
   | Direct (d,cu) ->
-      let cu = Future.chain ~pure:true cu (fun (c, u) -> hcons_constr c, u) in
+      (** Uncomment to check dynamically that all terms turned into
+          indirections are hashconsed. *)
+(* let check_hcons c = let c' = hcons_constr c in assert (c' == c); c in *)
+(* let cu = Future.chain ~pure:true cu (fun (c, u) -> check_hcons c; c, u) in *)
       let id = Int.Map.cardinal prfs in
       let prfs = Int.Map.add id (d,cu) prfs in
       let ndp =