diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml
index fecce595fe22b..8ae509e314e1c 100644
--- a/kernel/constant_typing.ml
+++ b/kernel/constant_typing.ml
@@ -214,7 +214,8 @@ let infer_parameter ~sec_univs env entry =
 
 let infer_definition ~sec_univs env entry =
   let env, usubst, _, univs = process_universes env entry.definition_entry_universes in
-  let j = Typeops.infer env entry.definition_entry_body in
+  let hbody = HConstr.of_constr env entry.definition_entry_body in
+  let j = Typeops.infer_hconstr env hbody in
   let typ = match entry.definition_entry_type with
     | None ->
       Vars.subst_univs_level_constr usubst j.uj_type
@@ -224,9 +225,10 @@ let infer_definition ~sec_univs env entry =
       Vars.subst_univs_level_constr usubst tj.utj_val
   in
   let body = Vars.subst_univs_level_constr usubst j.uj_val in
+  let hbody = if body == j.uj_val then Some hbody else None in
   let def = Def body in
   let hyps = used_section_variables env entry.definition_entry_secctx (Some body) typ in
-  {
+  hbody, {
     const_hyps = hyps;
     const_univ_hyps = make_univ_hyps sec_univs;
     const_body = def;
@@ -275,7 +277,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
   in
   (* Note: non-trivial trusted side-effects only in monomorphic case *)
   let body,env,ectx = skip_trusted_seff valid_signatures body env in
-  let j = Typeops.infer env body in
+  let hbody = HConstr.of_constr env body in
+  let j = Typeops.infer_hconstr env hbody in
   let j = unzip ectx j in
   let _ = Typeops.judge_of_cast env j DEFAULTcast tyj in
   let declared =
@@ -285,7 +288,8 @@ let check_delayed (type a) (handle : a effect_handler) tyenv (body : a proof_out
   let () = assert (Id.Set.equal declared declared') in
   (* Note: non-trivial usubst only in polymorphic case *)
   let def = Vars.subst_univs_level_constr usubst j.uj_val in
-  def, univs
+  let hbody = if def == j.uj_val && List.is_empty ectx then Some hbody else None in
+  hbody, def, univs
 
 (*s Global and local constant declaration. *)
 
diff --git a/kernel/constant_typing.mli b/kernel/constant_typing.mli
index b54e89142b63e..d15df0ea45316 100644
--- a/kernel/constant_typing.mli
+++ b/kernel/constant_typing.mli
@@ -39,10 +39,11 @@ val infer_parameter :
 
 val infer_definition :
   sec_univs:UVars.Instance.t option -> env -> definition_entry ->
-    ('a, unit) pconstant_body
+    HConstr.t option * ('a, unit) pconstant_body
 
 val infer_opaque :
   sec_univs:UVars.Instance.t option -> env -> 'a opaque_entry ->
     (unit, unit) pconstant_body * typing_context
 
-val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output -> (Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes)
+val check_delayed : 'a effect_handler -> typing_context -> 'a proof_output ->
+  HConstr.t option * Constr.t * Univ.ContextSet.t Opaqueproof.delayed_universes
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8face8549fc37..ed1ab91b84ed6 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -460,6 +460,10 @@ let destRef c = let open GlobRef in match kind c with
   | Construct (c,u) -> ConstructRef c, u
   | _ -> raise DestKO
 
+let destArray c = match kind c with
+  | Array (u,ar,def,ty) -> u,ar,def,ty
+  | _ -> raise DestKO
+
 (******************************************************************)
 (* Flattening and unflattening of embedded applications and casts *)
 (******************************************************************)
@@ -1322,6 +1326,25 @@ module Hannot = Hashcons.Make(Hannotinfo)
 
 let hcons_annot = Hashcons.simple_hcons Hannot.generate Hannot.hcons Name.hcons
 
+let dbg = CDebug.create ~name:"hcons" ()
+
+module GenHCons(C:sig
+    type t
+    val kind : t -> (t, t, Sorts.t, Instance.t, Sorts.relevance) kind_of_term
+    val self : t -> constr
+    val refcount : t -> int
+
+    val via_hconstr : bool
+
+    module Tbl : sig
+      val find_opt : t -> (constr * int) option
+      val add : t -> constr * int -> unit
+    end
+  end) = struct
+open C
+
+let steps = ref 0
+
 let rec hash_term (t : t) =
   match kind t with
   | Var i ->
@@ -1346,12 +1369,11 @@ let rec hash_term (t : t) =
     let c, hc = sh_rec c in
     (LetIn (hcons_annot na, b, t, c), combinesmall 6 (combine4 (hash_annot Name.hash na) hb ht hc))
   | App (c,l) ->
+    let _, cl = destApp (self t) in
     let c, hc = sh_rec c in
-    let l, hl = hash_term_array l in
+    let l, hl = hash_term_array cl l in
     (App (c,l), combinesmall 7 (combine hl hc))
-  | Evar (e,l) ->
-    let l, hl = hash_list_array l in
-    (Evar (e,l), combinesmall 8 (combine (Evar.hash e) hl))
+  | Evar _ -> assert false
   | Const (c,u) ->
     let c' = hcons_con c in
     let u', hu = Instance.share u in
@@ -1374,9 +1396,10 @@ let rec hash_term (t : t) =
       (lna, c), combine hna hc
     in
     let u, hu = Instance.share u in
-    let pms,hpms = hash_term_array pms in
+    let _,_,cpms,_,civ,_,_ = destCase (self t) in
+    let pms,hpms = hash_term_array cpms pms in
     let p, hp = hcons_ctx p in
-    let iv, hiv = sh_invert iv in
+    let iv, hiv = sh_invert civ iv in
     let c, hc = sh_rec c in
     let fold accu c =
       let c, h = hcons_ctx c in
@@ -1386,16 +1409,18 @@ let rec hash_term (t : t) =
     let hbl = combine (combine hc (combine hiv (combine hpms (combine hu hp)))) hbl in
     (Case (hcons_caseinfo ci, u, pms, (p,r), iv, c, bl), combinesmall 12 hbl)
   | Fix (ln,(lna,tl,bl)) ->
-    let bl,hbl = hash_term_array bl in
-    let tl,htl = hash_term_array tl in
+    let _, (_,ctl,cbl) = destFix (self t) in
+    let bl,hbl = hash_term_array cbl bl in
+    let tl,htl = hash_term_array ctl tl in
     let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
     let fold accu na = combine (hash_annot Name.hash na) accu in
     let hna = Array.fold_left fold 0 lna in
     let h = combine3 hna hbl htl in
     (Fix (ln,(lna,tl,bl)), combinesmall 13 h)
   | CoFix(ln,(lna,tl,bl)) ->
-    let bl,hbl = hash_term_array bl in
-    let tl,htl = hash_term_array tl in
+    let _, (_,ctl,cbl) = destCoFix (self t) in
+    let bl,hbl = hash_term_array cbl bl in
+    let tl,htl = hash_term_array ctl tl in
     let () = Array.iteri (fun i x -> Array.unsafe_set lna i (hcons_annot x)) lna in
     let fold accu na = combine (hash_annot Name.hash na) accu in
     let hna = Array.fold_left fold 0 lna in
@@ -1414,58 +1439,59 @@ let rec hash_term (t : t) =
     (t, combinesmall 18 (combine h l))
   | Float f as t -> (t, combinesmall 19 (Float64.hash f))
   | String s as t -> (t, combinesmall 20 (Pstring.hash s))
-  | Array (u,t,def,ty) ->
+  | Array (u,ar,def,ty) ->
+    let _,car,_,_ = destArray (self t) in
     let u, hu = Instance.share u in
-    let t, ht = hash_term_array t in
+    let t, ht = hash_term_array car ar in
     let def, hdef = sh_rec def in
     let ty, hty = sh_rec ty in
     let h = combine4 hu ht hdef hty in
     (Array(u,t,def,ty), combinesmall 21 h)
 
-and sh_invert = function
-  | NoInvert -> NoInvert, 0
-  | CaseInvert {indices;} ->
-    let indices, ha = hash_term_array indices in
+and sh_invert civ iv = match civ, iv with
+  | NoInvert, NoInvert -> NoInvert, 0
+  | CaseInvert {indices=cindices}, CaseInvert {indices;} ->
+    let indices, ha = hash_term_array cindices indices in
     CaseInvert {indices;}, combinesmall 1 ha
+  | (NoInvert | CaseInvert _), _ -> assert false
 
-and sh_rec t =
+and sh_rec_main t =
   let (y, h) = hash_term t in
   (HashsetTerm.repr h (T y) term_table, h)
 
+and sh_rec t =
+  incr steps;
+  if refcount t = 1 then sh_rec_main t
+  else match Tbl.find_opt t with
+    | Some res -> res
+    | None ->
+      let res = sh_rec_main t in
+      Tbl.add t res;
+      res
+
 (* Note : During hash-cons of arrays, we modify them *in place* *)
 
-and hash_term_array t =
+and hash_term_array ct t =
   let accu = ref 0 in
   for i = 0 to Array.length t - 1 do
     let x, h = sh_rec (Array.unsafe_get t i) in
     accu := combine !accu h;
-    Array.unsafe_set t i x
+    Array.unsafe_set ct i x
   done;
   let h = !accu in
-  (HashsetTermArray.repr h t term_array_table, h)
-
-and hash_list_array l =
-  let fold accu c =
-    let c, h = sh_rec c in
-    (combine accu h, c)
-  in
-  let h, l = SList.Smart.fold_left_map fold 0 l in
-  (l, h)
-
-  (* Make sure our statically allocated Rels (1 to 16) are considered
-     as canonical, and hence hash-consed to themselves *)
-let () = ignore (hash_term_array rels)
+  (HashsetTermArray.repr h ct term_array_table, h)
 
 let hcons t = NewProfile.profile "Constr.hcons" (fun () -> fst (sh_rec t)) ()
 
-let dbg = CDebug.create ~name:"hcons" ()
-
 let hcons t =
+  steps := 0;
   let t = hcons t in
   dbg Pp.(fun () ->
       let open Hashset in
       let stats = HashsetTerm.stats term_table in
       v 0 (
+        str "via hconstr = " ++ bool via_hconstr ++ spc() ++
+        str "steps = " ++ int !steps ++ spc() ++
         str "num_bindings = " ++ int stats.num_bindings ++ spc() ++
         str "num_buckets = " ++ int stats.num_buckets ++ spc() ++
         str "max_bucket_length = " ++ int stats.max_bucket_length
@@ -1473,6 +1499,28 @@ let hcons t =
     );
   t
 
+end
+
+module HCons = GenHCons(struct
+    type t = constr
+    let kind = kind
+    let self x = x
+    let refcount _ = 1
+
+    let via_hconstr = false
+
+    module Tbl = struct
+      let find_opt _ = None
+      let add _ _ : unit = assert false
+    end
+  end)
+
+  (* Make sure our statically allocated Rels (1 to 16) are considered
+     as canonical, and hence hash-consed to themselves *)
+let () = ignore (HCons.hash_term_array rels rels)
+
+let hcons = HCons.hcons
+
 (* let hcons_types = hcons_constr *)
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
diff --git a/kernel/constr.mli b/kernel/constr.mli
index f1d480724039f..629c655f01719 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -628,6 +628,23 @@ val case_info_hash : case_info -> int
 
 (*********************************************************************)
 
+module GenHCons(C:sig
+    type t
+    val kind : t -> (t, t, Sorts.t, UVars.Instance.t, Sorts.relevance) kind_of_term
+    val self : t -> constr
+    val refcount : t -> int
+
+    val via_hconstr : bool
+
+    module Tbl : sig
+      val find_opt : t -> (constr * int) option
+      val add : t -> constr * int -> unit
+    end
+  end) : sig
+  val hcons : C.t -> constr
+end
+
+
 val hcons : constr -> constr
 
 val hasheq_kind : (_ kind_of_term as 'k) -> 'k -> bool
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 0ed78b044b93c..7a34a9c01e8b7 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -136,12 +136,12 @@ let hcons_rel_decl =
 
 let hcons_rel_context l = List.Smart.map hcons_rel_decl l
 
-let hcons_const_def = function
+let hcons_const_def ?(hbody=Constr.hcons) = function
   | Undef inl -> Undef inl
   | Primitive p -> Primitive p
   | Symbol r -> Symbol r
   | Def l_constr ->
-    Def (Constr.hcons l_constr)
+    Def (hbody l_constr)
   | OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
 
 let hcons_universes cbu =
@@ -150,9 +150,9 @@ let hcons_universes cbu =
   | Polymorphic ctx ->
     Polymorphic (UVars.hcons_abstract_universe_context ctx)
 
-let hcons_const_body cb =
+let hcons_const_body ?hbody cb =
   { cb with
-    const_body = hcons_const_def cb.const_body;
+    const_body = hcons_const_def ?hbody cb.const_body;
     const_type = Constr.hcons cb.const_type;
     const_universes = hcons_universes cb.const_universes;
   }
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 84be152b80964..7b3be4bf1973f 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -88,7 +88,8 @@ val safe_flags : Conv_oracle.oracle -> typing_flags
     of the structure, but simply hash-cons all inner constr
     and other known elements *)
 
-val hcons_const_body : ('a, 'b) pconstant_body -> ('a, 'b) pconstant_body
+val hcons_const_body : ?hbody:(Constr.t -> Constr.t) ->
+  ('a, 'b) pconstant_body -> ('a, 'b) pconstant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
 val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/hConstr.ml b/kernel/hConstr.ml
index 1b568e37a53fb..53b8ce2762a29 100644
--- a/kernel/hConstr.ml
+++ b/kernel/hConstr.ml
@@ -384,3 +384,18 @@ let of_constr env c =
 let of_constr env c = NewProfile.profile "HConstr.of_constr" (fun () -> of_constr env c) ()
 
 let kind x = x.kind
+
+let hcons x =
+  let tbl = Tbl.create 47 in
+  let module HCons = GenHCons(struct
+      type nonrec t = t
+      let kind = kind
+      let self = self
+      let refcount = refcount
+        let via_hconstr = true
+      module Tbl = struct
+        let find_opt x = Tbl.find_opt tbl x
+        let add x y = Tbl.add tbl x y
+      end
+    end) in
+  HCons.hcons x
diff --git a/kernel/hConstr.mli b/kernel/hConstr.mli
index 08c4c12f1ef3d..b1e0cfe7f8125 100644
--- a/kernel/hConstr.mli
+++ b/kernel/hConstr.mli
@@ -57,3 +57,5 @@ module Tbl : sig
 
   val create : int -> 'a t
 end
+
+val hcons : t -> Constr.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9d3b464c72fe6..039760999cbfa 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -662,11 +662,19 @@ let push_const_bytecode senv cb =
   let senv = set_vm_library vmtab senv in
   senv, cb
 
-let add_constant_aux senv (kn, cb) =
+let make_hbody = function
+  | None -> None
+  | Some hc -> Some (fun c ->
+      assert (c == HConstr.self hc);
+      HConstr.hcons hc)
+
+let add_constant_aux senv ?hbody (kn, cb) =
   let l = Constant.label kn in
   (* This is the only place where we hashcons the contents of a constant body *)
   let senv, cb = push_const_bytecode senv cb in
-  let cb = if sections_are_opened senv then cb else Declareops.hcons_const_body cb in
+  let cb = if sections_are_opened senv then cb else
+      Declareops.hcons_const_body ?hbody:(make_hbody hbody) cb
+  in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
   let senv'' = match cb.const_body with
     | Undef (Some lev) ->
@@ -830,7 +838,7 @@ let infer_direct_opaque ~sec_univs env ce =
   let cb, ctx = Constant_typing.infer_opaque ~sec_univs env ce in
   let body = ce.Entries.opaque_entry_body, Univ.ContextSet.empty in
   let handle _env c () = (c, Univ.ContextSet.empty, 0) in
-  let (c, u) = Constant_typing.check_delayed handle ctx (body, ()) in
+  let (_hbody, c, u) = Constant_typing.check_delayed handle ctx (body, ()) in
   (* No constraints can be generated, we set it empty everywhere *)
   let () = assert (is_empty_private u) in
   { cb with const_body = OpaqueDef c }
@@ -864,11 +872,11 @@ let export_side_effects senv eff =
         let univs = Univ.ContextSet.union uctx univs in
         let env, cb =
           let ce = constant_entry_of_side_effect eff in
-          let cb = match ce with
+          let _hbody, cb = match ce with
             | DefinitionEff ce ->
               Constant_typing.infer_definition ~sec_univs env ce
             | OpaqueEff ce ->
-              infer_direct_opaque ~sec_univs env ce
+              None, infer_direct_opaque ~sec_univs env ce
           in
           let cb = compile_bytecode env cb in
           let eff = { eff with seff_body = cb } in
@@ -910,7 +918,7 @@ let export_private_constants eff senv =
 
 let add_constant l decl senv =
   let kn = Constant.make2 senv.modpath l in
-  let senv, cb =
+  let senv, (hbody, cb) =
     let sec_univs = Option.map Section.all_poly_univs senv.sections in
       match decl with
       | Entries.OpaqueEntry ce ->
@@ -921,23 +929,23 @@ let add_constant l decl senv =
         let nonce = Nonce.create () in
         let future_cst = HandleMap.add i (ctx, senv, nonce) senv.future_cst in
         let senv = { senv with future_cst } in
-        senv, { cb with const_body = OpaqueDef o }
+        senv, (None, { cb with const_body = OpaqueDef o })
       | Entries.DefinitionEntry entry ->
         senv, Constant_typing.infer_definition ~sec_univs senv.env entry
       | Entries.ParameterEntry entry ->
-        senv, Constant_typing.infer_parameter ~sec_univs senv.env entry
+        senv, (None, Constant_typing.infer_parameter ~sec_univs senv.env entry)
       | Entries.PrimitiveEntry entry ->
         let senv = match entry with
         | { Entries.prim_entry_content = CPrimitives.OT_type t; _ } ->
           if sections_are_opened senv then CErrors.anomaly (Pp.str "Primitive type not allowed in sections");
           add_retroknowledge (Retroknowledge.Register_type(t,kn)) senv
         | _ -> senv in
-        senv, Constant_typing.infer_primitive senv.env entry
+        senv, (None, Constant_typing.infer_primitive senv.env entry)
       | Entries.SymbolEntry entry ->
-        senv, Constant_typing.infer_symbol senv.env entry
+        senv, (None, Constant_typing.infer_symbol senv.env entry)
   in
   let cb = compile_bytecode senv.env cb in
-  let senv = add_constant_aux senv (kn, cb) in
+  let senv = add_constant_aux senv ?hbody (kn, cb) in
   kn, senv
 
 let add_constant ?typing_flags l decl senv =
@@ -965,8 +973,11 @@ let check_opaque senv (i : Opaqueproof.opaque_handle) pf =
     in
     body, uctx, trusted
   in
-  let (c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in
-  let c = Constr.hcons c in
+  let (hbody, c, ctx) = Constant_typing.check_delayed handle ty_ctx pf in
+  let c = match hbody with
+    | Some hbody -> assert (c == HConstr.self hbody); HConstr.hcons hbody
+    | None -> Constr.hcons c
+  in
   let ctx = match ctx with
   | Opaqueproof.PrivateMonomorphic u ->
     Opaqueproof.PrivateMonomorphic (Univ.hcons_universe_context_set u)
@@ -1007,12 +1018,12 @@ let check_constraints uctx = function
 let add_private_constant l uctx decl senv : (Constant.t * private_constants) * safe_environment =
   let kn = Constant.make2 senv.modpath l in
   let senv = push_context_set ~strict:true uctx senv in
-    let cb =
+    let hbody, cb =
       let sec_univs = Option.map Section.all_poly_univs senv.sections in
       match decl with
       | OpaqueEff ce ->
         let () = assert (check_constraints uctx ce.Entries.opaque_entry_universes) in
-        infer_direct_opaque ~sec_univs senv.env ce
+        None, infer_direct_opaque ~sec_univs senv.env ce
       | DefinitionEff ce ->
         let () = assert (check_constraints uctx ce.Entries.definition_entry_universes) in
         Constant_typing.infer_definition ~sec_univs senv.env ce
@@ -1028,7 +1039,7 @@ let add_private_constant l uctx decl senv : (Constant.t * private_constants) * s
     { cb with const_body = Undef None }
   | Undef _ | Primitive _ | Symbol _ -> assert false
   in
-  let senv = add_constant_aux senv (kn, dcb) in
+  let senv = add_constant_aux senv ?hbody (kn, dcb) in
   let eff =
     let from_env = CEphemeron.create (Certificate.make senv) in
     let eff = {
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 26da7c678c7fd..ef5ccb03fbc1e 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -856,8 +856,7 @@ and execute_array tbl env cs =
   Array.map (fun c -> execute tbl env c) cs
 
 let execute env c =
-  let c = HConstr.of_constr env c in
-  NewProfile.profile "Typeops.execute" (fun () -> c, execute (HConstr.Tbl.create 57) env c) ()
+  NewProfile.profile "Typeops.execute" (fun () -> execute (HConstr.Tbl.create 57) env c) ()
 
 (* Derived functions *)
 
@@ -877,12 +876,16 @@ let check_wellformed_universes env c =
 let check_wellformed_universes env c =
   NewProfile.profile "check-wf-univs" (fun () -> check_wellformed_universes env c) ()
 
-let infer env constr =
-  let () = check_wellformed_universes env constr in
-  let hconstr, t = execute env constr in
+let infer_hconstr env hconstr =
   let constr = HConstr.self hconstr in
+  let () = check_wellformed_universes env constr in
+  let t = execute env hconstr in
   make_judge constr t
 
+let infer env c =
+  let c = HConstr.of_constr env c in
+  infer_hconstr env c
+
 let assumption_of_judgment env {uj_val=c; uj_type=t} =
   infer_assumption env c t
 
@@ -892,8 +895,9 @@ let type_judgment env {uj_val=c; uj_type=t} =
 
 let infer_type env constr =
   let () = check_wellformed_universes env constr in
-  let hconstr, t = execute env constr in
+  let hconstr = HConstr.of_constr env constr in
   let constr = HConstr.self hconstr in
+  let t = execute env hconstr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 1e40b77b77b86..42fdcf9cd068a 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -25,6 +25,7 @@ open Environ
    Do not discard the result. *)
 
 val infer      : env -> constr       -> unsafe_judgment
+val infer_hconstr : env -> HConstr.t -> unsafe_judgment
 val infer_type : env -> types        -> unsafe_type_judgment
 
 val check_context :