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/cooking.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/cooking.mli')
| -rw-r--r-- | kernel/cooking.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.mli b/kernel/cooking.mli index eb4073096..7d47eba23 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,7 @@ type result = bool * constant_universes * inline * Context.Named.t option -val cook_constant : env -> recipe -> result +val cook_constant : hcons:bool -> env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr (** {6 Utility functions used in module [Discharge]. } *) |