diff --git a/dev/ci/user-overlays/17576-SkySkimmer-let-abstract.sh b/dev/ci/user-overlays/17576-SkySkimmer-let-abstract.sh new file mode 100644 index 000000000000..758b59b4fe6b --- /dev/null +++ b/dev/ci/user-overlays/17576-SkySkimmer-let-abstract.sh @@ -0,0 +1 @@ +overlay metacoq https://github.com/SkySkimmer/metacoq let-abstract 17576 diff --git a/doc/changelog/08-vernac-commands-and-options/17576-let-abstract.rst b/doc/changelog/08-vernac-commands-and-options/17576-let-abstract.rst new file mode 100644 index 000000000000..851c683dc2b9 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/17576-let-abstract.rst @@ -0,0 +1,6 @@ +- **Changed:** + :cmd:`Let` with :cmd:`Qed` produces an opaque side definition + instead of being treated as a transparent `let` after the section is closed. + The previous behaviour can be recovered using :attr:`clearbody` and :cmd:`Defined` + (`#17576 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 73d3f60bfd19..fe86d6b543f3 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -75,10 +75,15 @@ usable outside the section as shown in this :ref:`example A. +Check bar' : forall A, A -> A. diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 5097ac97fe29..bced9ebddb51 100644 --- a/vernac/comAssumption.ml +++ b/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 diff --git a/vernac/declare.ml b/vernac/declare.ml index 14eb57542308..20d3195b89ac 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -486,15 +486,7 @@ let objVariable : Id.t Libobject.Dyn.tag = let inVariable v = Libobject.Dyn.Easy.inj v objVariable -let warn_opaque_let = CWarnings.create ~name:"opaque-let" ~category:Deprecation.Version.v8_18 - Pp.(fun name -> - Id.print name ++ - strbrk " is declared opaque (Qed) but this is not fully respected" ++ - strbrk " inside the section and not at all outside the section." ++ fnl() ++ - strbrk "Use attribute #[clearbody] to get the current behaviour of clearing" ++ - strbrk " the body at the start of proofs in a forward compatible way.") - -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)); @@ -521,14 +513,34 @@ 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 - (* NB: de.proof_entry_secctx is ignored *) - 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_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 + (* opaque implies clearbody, so we don't see useless "foo := foo_subproof" in the context *) Glob_term.Explicit, opaque || clearbody, de.proof_entry_universes in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); @@ -537,8 +549,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 *) @@ -666,7 +678,7 @@ let declare_entry_core ~name ?(scope=Locality.default_scope) ?(clearbody=false) in let dref = match scope with | Locality.Discharge -> - let () = declare_variable_core ~name ~kind (SectionLocalDef {clearbody; entry}) in + let () = declare_variable_core ~typing_flags ~name ~kind (SectionLocalDef {clearbody; entry}) in if should_suggest then Proof_using.suggest_variable (Global.env ()) name; Names.GlobRef.VarRef name | Locality.Global local -> @@ -1652,6 +1664,8 @@ let get_recnames pf = else [] +let definition_scope ps = ps.pinfo.info.scope + let set_used_variables ps ~using = let open Context.Named.Declaration in let env = Global.env () in diff --git a/vernac/declare.mli b/vernac/declare.mli index c9bc46662d08..51f9a4789334 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -256,6 +256,8 @@ module Proof : sig (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : Genarg.glob_generic_argument -> t -> t + val definition_scope : t -> Locality.definition_scope + (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) *) val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t @@ -386,6 +388,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 diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index a7b53506cc97..490295119a61 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -570,7 +570,7 @@ let program_inference_hook env sigma ev = user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") -let vernac_set_used_variables ~pstate using : Declare.Proof.t = +let vernac_set_used_variables pstate using : Declare.Proof.t = let env = Global.env () in let sigma, _ = Declare.Proof.get_current_context pstate in let fixnames = Declare.Proof.get_recnames pstate in @@ -583,7 +583,7 @@ let vernac_set_used_variables ~pstate using : Declare.Proof.t = let vernac_set_used_variables_opt ?using pstate = match using with | None -> pstate - | Some expr -> vernac_set_used_variables ~pstate expr + | Some expr -> vernac_set_used_variables pstate expr (* XXX: Interpretation of lemma command, duplication with ComFixpoint / ComDefinition ? *) @@ -1491,7 +1491,7 @@ let vernac_existing_class id = let command_focus = Proof.new_focus_kind () let focus_command_cond = Proof.no_cond command_focus -let vernac_set_end_tac ~pstate tac = +let vernac_set_end_tac pstate tac = let env = Genintern.empty_glob_sign ~strict:true (Global.env ()) in let _, tac = Genintern.generic_intern env tac in (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) @@ -2208,6 +2208,25 @@ let vernac_validate_proof ~pstate = str "No issues found." else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues) +let vernac_proof pstate tac using = + let is_let = match Declare.Proof.definition_scope pstate with + | Discharge -> true + | Global _ -> false + in + let using = if not is_let then Option.append using (Proof_using.get_default_proof_using ()) + else + let () = if Option.has_some using + then CErrors.user_err Pp.(str "Let does not support Proof using.") + in + None + in + let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in + let usings = if Option.is_empty using then "using:no" else "using:yes" in + Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); + let pstate = Option.fold_left vernac_set_end_tac pstate tac in + let pstate = Option.fold_left vernac_set_used_variables pstate using in + pstate + let translate_vernac_synterp ?loc ~atts v = let open Vernactypes in match v with | EVernacNotation { local; decl } -> vtdefault(fun () -> Metasyntax.add_notation_interpretation ~local (Global.env()) decl) @@ -2535,12 +2554,7 @@ let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with | VernacProof (tac, using) -> vtmodifyproof(fun ~pstate -> unsupported_attributes atts; - let using = Option.append using (Proof_using.get_default_proof_using ()) in - let tacs = if Option.is_empty tac then "tac:no" else "tac:yes" in - let usings = if Option.is_empty using then "using:no" else "using:yes" in - Aux_file.record_in_aux_at "VernacProof" (tacs^" "^usings); - let pstate = Option.cata (vernac_set_end_tac ~pstate) pstate tac in - Option.cata (vernac_set_used_variables ~pstate) pstate using) + vernac_proof pstate tac using) | VernacEndProof pe -> unsupported_attributes atts;