5 files changed, 19 insertions, 8 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f5059cd750..a9f212393e 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -191,15 +191,19 @@ let lift_univs cb subst =
       subst, Univ.UContext.make (inst,cstrs')
   else subst, cb.const_universes
 
-let cook_constant env { from = cb; info } =
+let cook_constant ~hcons env { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
   let usubst, univs = lift_univs cb usubst in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
+  let map c =
+    let c = abstract_constant_body (expmod c) hyps in
+    if hcons then hcons_constr c else c
+  in
   let body = on_body modlist (hyps, usubst, abs_ctx)
-    (fun c -> abstract_constant_body (expmod c) hyps)
+    map
     cb.const_body
   in
   let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index eb40730969..7d47eba23e 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]. } *)
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index f147ea3433..74ba73508c 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 =
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 5139cf0512..3897d5e51e 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
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2eb2c040e1..2eba1eb2a7 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -186,7 +186,8 @@ let rec unzip ctx j =
       unzip ctx { j with uj_val = mkApp (mkLambda (n,ty,j.uj_val),arg) }
 
 let hcons_j j =
-  { uj_val = hcons_constr j.uj_val; uj_type = hcons_constr j.uj_type} 
+  (** Do not hashcons type: it is not used by the callers of this function. *)
+  { uj_val = hcons_constr j.uj_val; uj_type = j.uj_type} 
 
 let feedback_completion_typecheck =
   let open Feedback in
@@ -507,7 +508,9 @@ let translate_local_assum env t =
     t
 
 let translate_recipe env kn r =
-  build_constant_declaration kn env (Cooking.cook_constant env r)
+  let (_, dir, _) = Constant.repr3 kn in
+  let hcons = DirPath.is_empty dir in
+  build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
 
 let translate_local_def mb env id centry =
   let def,typ,proj,poly,univs,inline_code,ctx =