From ff996b19faeff112a156f5db6c9ab9f26e855145 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 27 Mar 2017 00:22:51 +0200 Subject: 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. --- kernel/opaqueproof.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel/opaqueproof.ml') 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 = -- cgit v1.2.3