diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-27 00:22:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-03-27 11:32:16 +0200 |
| commit | ff996b19faeff112a156f5db6c9ab9f26e855145 (patch) | |
| tree | d5921b7ff9df606a0ff3fcb3830ab12af307eb91 /kernel/opaqueproof.mli | |
| parent | 7535e268f7706d1dee263fdbafadf920349103db (diff) | |
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.
Diffstat (limited to 'kernel/opaqueproof.mli')
| -rw-r--r-- | kernel/opaqueproof.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 5139cf051..3897d5e51 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -28,8 +28,9 @@ val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) val create : proofterm -> opaque -(** Turn a direct [opaque] into an indirect one, also hashconses constr. - * The integer is an hint of the maximum id used so far *) +(** Turn a direct [opaque] into an indirect one. It is your responsibility to + hashcons the inner term beforehand. The integer is an hint of the maximum id + used so far *) val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab (** From a [opaque] back to a [constr]. This might use the |