Let with Qed: produce really-Qed side definition

cf discussion in #17544

This does have a tradeoff as the side definition still exists after
the section is closed unlike usual.

vernac/comAssumption.ml

@@ -22,7 +22,7 @@ module RelDecl = Context.Rel.Declaration
 
 let declare_variable is_coe ~kind typ univs imps impl {CAst.v=name} =
   let kind = Decls.IsAssumption kind in
-  let () = Declare.declare_variable ~name ~kind ~typ ~impl ~univs in
+  let () = Declare.declare_variable ~name ~kind ~typing_flags:None ~typ ~impl ~univs in
   let () = Declare.assumption_message name in
   let r = GlobRef.VarRef name in
   let () = maybe_declare_manual_implicits true r imps in

vernac/declare.ml

@@ -489,7 +489,7 @@ let warn_opaque_let = CWarnings.create ~name:"opaque-let" ~category:"fragile"
     strbrk " is declared opaque but this is not fully respected" ++
     strbrk " inside the section and not at all outside the section.")
 
-let declare_variable_core ~name ~kind d =
+let declare_variable_core ~name ~kind ~typing_flags d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
     raise (DeclareUniv.AlreadyDeclared (None, name));
@@ -516,13 +516,35 @@ let declare_variable_core ~name ~kind d =
       (* We must declare the universe constraints before type-checking the
          term. *)
       let () = DeclareUctx.declare_universe_context ~poly univs in
-      let se = {
+      let opaque = de.proof_entry_opaque in
+      let se = if opaque then
+          let cname = Id.of_string (Id.to_string name ^ "_subproof") in
+          let cname = Namegen.next_global_ident_away cname Id.Set.empty in
+          let de = {
+            proof_entry_body = Future.from_val ((body, Univ.ContextSet.empty), Evd.empty_side_effects);
+            proof_entry_secctx = de.proof_entry_secctx;
+            proof_entry_feedback = de.proof_entry_feedback;
+            proof_entry_type = de.proof_entry_type;
+            proof_entry_universes = UState.univ_entry ~poly UState.empty;
+            proof_entry_opaque = true;
+            proof_entry_inline_code = de.proof_entry_inline_code;
+          }
+          in
+          let kn = declare_constant ~name:cname
+              ~local:ImportNeedQualified ~kind:(IsProof Lemma) ~typing_flags
+              (DefinitionEntry de)
+          in
+          {
+            Entries.secdef_body = Constr.mkConstU (kn, Univ.Instance.empty);
+            secdef_secctx = de.proof_entry_secctx;
+            secdef_type = None;
+          }
+        else {
         Entries.secdef_body = body;
         secdef_secctx = de.proof_entry_secctx;
         secdef_type = de.proof_entry_type;
       } in
       let () = Global.push_named_def (name, se) in
-      let opaque = de.proof_entry_opaque in
       let () = if opaque then warn_opaque_let name in
       Glob_term.Explicit, opaque, de.proof_entry_universes
   in
@@ -532,8 +554,8 @@ let declare_variable_core ~name ~kind d =
   Impargs.declare_var_implicits ~impl name;
   Notation.declare_ref_arguments_scope (GlobRef.VarRef name)
 
-let declare_variable ~name ~kind ~typ ~impl ~univs =
-  declare_variable_core ~name ~kind (SectionLocalAssum { typ; impl; univs })
+let declare_variable ~name ~kind ~typing_flags ~typ ~impl ~univs =
+  declare_variable_core ~name ~kind ~typing_flags (SectionLocalAssum { typ; impl; univs })
 
 (* Declaration messages *)
 
@@ -661,7 +683,7 @@ let declare_entry_core ~name ?(scope=Locality.default_scope) ~kind ~typing_flags
   in
   let dref = match scope with
   | Locality.Discharge ->
-    let () = declare_variable_core ~name ~kind (SectionLocalDef entry) in
+    let () = declare_variable_core ~typing_flags ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Locality.Global local ->

vernac/declare.mli

@@ -380,6 +380,7 @@ val declare_entry
 val declare_variable
   :  name:variable
   -> kind:Decls.logical_kind
+  -> typing_flags:Declarations.typing_flags option
   -> typ:Constr.types
   -> impl:Glob_term.binding_kind
   -> univs:UState.named_universes_entry