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.

kernel/entries.mli

@@ -77,7 +77,6 @@ type definition_entry = {
 
 type section_def_entry = {
   secdef_body : constr;
-  secdef_secctx : Id.Set.t option;
   secdef_type : types option;
 }
 

kernel/term_typing.ml

@@ -317,22 +317,15 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     j.uj_val, t
 
-let translate_local_def env _id centry =
-  let centry = {
-    const_entry_body = centry.secdef_body;
-    const_entry_secctx = centry.secdef_secctx;
-    const_entry_type = centry.secdef_type;
-    const_entry_universes = Monomorphic_entry;
-    const_entry_inline_code = false;
-  } in
-  let decl = infer_constant ~sec_univs:None env (DefinitionEntry centry) in
-  let typ = decl.cook_type in
-  let () = match decl.cook_universes with
-  | Monomorphic -> ()
-  | Polymorphic _ -> assert false
-  in
-  let c = match decl.cook_body with
-  | Def c -> c
-  | Undef _ | Primitive _ | OpaqueDef _ -> assert false
+let translate_local_def env _id { secdef_body; secdef_type; } =
+  let j = Typeops.infer env secdef_body in
+  let typ = match secdef_type with
+    | None -> j.uj_type
+    | Some typ ->
+      let tj = Typeops.infer_type env typ in
+      let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
+      tj.utj_val
   in
-  c, decl.cook_relevance, typ
+  let c = j.uj_val in
+  let r = Relevanceops.relevance_of_term env c in
+  c, r, typ

test-suite/bugs/bug_17576_1.v

@@ -0,0 +1,32 @@
+(* Let doesn't respect (default) Proof using *)
+
+(* Maybe we will want to change this behaviour someday
+   but keep in mind that if we do then "bar'" should somehow get 2 A arguments.
+*)
+
+Set Default Proof Using "Type".
+Set Warnings "-opaque-let".
+
+Section S.
+
+  Variable A : Type.
+  Variable a : A.
+
+  Let foo : A.
+  Proof. exact a. Qed.
+
+  Definition bar := foo.
+
+  Variable b : A.
+
+  Let foo' : A.
+  Proof using a b.
+    exact b.
+  Qed.
+
+  Definition bar' := foo'.
+
+End S.
+
+Check bar : forall A, A -> A.
+Check bar' : forall A, A -> A.

test-suite/output/UnivBinders.out

@@ -73,8 +73,7 @@ File "./output/UnivBinders.v", line 78, characters 47-51:
 Warning: ff is declared opaque but this is not fully respected inside the
 section and not at all outside the section. [opaque-let,fragile]
 bobmorane =
-let tt := Type@{UnivBinders.32} in
-let ff := Type@{UnivBinders.34} in tt -> ff
+let tt := Type@{UnivBinders.32} in let ff := ff_subproof in tt -> ff
      : Type@{max(UnivBinders.31,UnivBinders.33)}
 File "./output/UnivBinders.v", line 85, characters 23-25:
 The command has indeed failed with message:

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

@@ -491,7 +491,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));
@@ -505,7 +505,7 @@ let declare_variable_core ~name ~kind d =
       let () = DeclareUctx.declare_universe_context ~poly uctx in
       let () = Global.push_named_assum (name,typ) in
       impl, true, univs
-    | SectionLocalDef (de) ->
+    | SectionLocalDef de ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
       let ((body, body_uctx), eff) = Future.force de.proof_entry_body in
@@ -518,13 +518,33 @@ 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 = None; (* de.proof_entry_secctx is NOT respected *)
+            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_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
@@ -534,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 *)
 
@@ -663,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

@@ -382,6 +382,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