also use hconstr to hcons Qed bodies

kernel/constant_typing.ml

@@ -277,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 =
@@ -287,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. *)
 

kernel/constant_typing.mli

@@ -45,4 +45,5 @@ 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

kernel/safe_typing.ml

@@ -838,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 }
@@ -973,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)