From f8b888282d180f9284bebfa489485b63f9f9556e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 10 Jun 2026 14:08:09 +0200 Subject: [PATCH 1/6] Proof using correctly handle non secvars in the env --- kernel/environ.ml | 4 ++++ kernel/environ.mli | 3 +++ test-suite/bugs/bug_12608.v | 9 ++++++++ vernac/declare.ml | 31 ++++++++------------------- vernac/proof_using.ml | 42 ++++++++++++++++--------------------- vernac/proof_using.mli | 1 - 6 files changed, 43 insertions(+), 47 deletions(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 08284ffa1450..98681d9656e6 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -224,6 +224,10 @@ let var_status_ctxt ?(check=true) id ctxt = let var_status ?check id env = var_status_ctxt ?check id env.env_named_context +let section_variables_ctxt ctxt = ctxt.env_named_secvars + +let section_variables env = section_variables_ctxt env.env_named_context + let match_named_context_val c = match c.env_named_ctx with | [] -> None | decl :: ctx -> diff --git a/kernel/environ.mli b/kernel/environ.mli index b712e764aa07..efafa701f672 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -109,6 +109,9 @@ val var_status_eq : var_status -> var_status -> bool val var_status_ctxt : ?check:bool -> Id.t -> named_context_val -> var_status val var_status : ?check:bool -> Id.t -> env -> var_status +val section_variables_ctxt : named_context_val -> Id.Set.t +val section_variables : env -> Id.Set.t + val named_context_of_val : named_context_val -> Constr.named_context val val_of_named_context : (var_status * Constr.named_declaration) list -> named_context_val val empty_named_context_val : named_context_val diff --git a/test-suite/bugs/bug_12608.v b/test-suite/bugs/bug_12608.v index bad2361b49df..591d91c8d071 100644 --- a/test-suite/bugs/bug_12608.v +++ b/test-suite/bugs/bug_12608.v @@ -19,4 +19,13 @@ Section S. Unshelve. all:exact n. Qed. + + Variable A : Type. + + Derive X : A -> A in (X = X) as H. + Proof using Type*. + reflexivity. + Unshelve. + exact (fun x => x). + Qed. End S. diff --git a/vernac/declare.ml b/vernac/declare.ml index a7fa69557df4..d29422a4fb63 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -962,26 +962,22 @@ let declare_parameter ~loc ~name ~scope ~hook ~impargs ~uctx pe = (* Using processing *) let interp_proof_using_gen f env evd cinfo using = - let cextract v (fixnames, terms) = - let name, new_terms = f v in - name :: fixnames, new_terms @ terms - in - let fixnames, terms = CList.fold_right cextract cinfo ([],[]) in - Proof_using.definition_using env evd ~fixnames ~terms ~using + let terms = CList.concat_map f cinfo in + Proof_using.definition_using env evd ~terms ~using let interp_proof_using_cinfo env evd cinfo using = - let f { CInfo.name; typ; _ } = name, [typ] in + let f { CInfo.typ; _ } = [typ] in interp_proof_using_gen f env evd cinfo using -let gather_mutual_using_data cinfo = - List.fold_left2 (fun acc CInfo.{name} (body, typ) -> +let gather_mutual_using_data bodies_types = + List.fold_left (fun acc (body, typ) -> let l = Option.List.flatten EConstr.[Option.map of_constr typ; Some (of_constr body)] in - (name, l) :: acc) [] cinfo + l :: acc) [] bodies_types let interp_mutual_using env cinfo bodies_types using = let evd = Evd.from_env env in Option.map (fun using -> - let cinfos = gather_mutual_using_data cinfo bodies_types in + let cinfos = gather_mutual_using_data bodies_types in let f x = x in interp_proof_using_gen f env evd cinfos using) using @@ -2007,21 +2003,13 @@ let set_used_variables ps ~using = CErrors.user_err Pp.(str "Used section variables can be declared only once"); ctx, { ps with using = Some (Context.Named.to_vars ctx) } -(* Interprets the expression in the current proof context, from vernacentries *) -let get_recnames pf = - if Option.has_some pf.pinfo.Proof_info.possible_guard then - List.map (fun c -> c.CInfo.name) pf.pinfo.Proof_info.cinfo - else - [] - let interpret_proof_using pstate using = let env = Global.env () in let pf = get pstate in let sigma, _ = Proof.get_proof_context pf in - let fixnames = get_recnames pstate in let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in let terms = List.map pi3 (initial_goals (get pstate)) in - Proof_using.definition_using env sigma ~fixnames ~using ~terms + Proof_using.definition_using env sigma ~using ~terms let set_proof_using pstate using = let using = interpret_proof_using pstate using in @@ -2595,8 +2583,7 @@ let solve_obligation ?check_final prg num tac = let using = let using = Internal.get_using prg in let env = Global.env () in - let f {CInfo.name; typ; _} = name, [typ] in - Option.map (interp_proof_using_gen f env evd [cinfo]) using + Option.map (interp_proof_using_cinfo env evd [cinfo]) using in let poly = Internal.get_poly prg in let info = Info.make ~kind ~poly () in diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index c9d0366ab786..1ed1e74422dc 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -36,15 +36,12 @@ let rec close_fwd env sigma s = in if Id.Set.equal s s' then s else close_fwd env sigma s' -let set_of_type env sigma fixnames ty = - List.fold_right Id.Set.remove fixnames - (List.fold_left (fun acc ty -> +let set_of_type env sigma ty = + let s = List.fold_left (fun acc ty -> Id.Set.union (Termops.global_vars_set env sigma ty) acc) - Id.Set.empty ty) - -let full_set fixnames env = - let add id ids = if List.mem_f Id.equal id fixnames then ids else Id.Set.add id ids in - List.fold_right add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty + Id.Set.empty ty + in + Id.Set.inter s (Environ.section_variables env) let warn_all_collection_precedence = CWarnings.create ~name:"all-collection-precedence" ~category:Deprecation.Version.v8_15 Pp.(fun () -> str "Variable " ++ Id.print all_collection_id ++ str " is shadowed by Collection named " ++ Id.print all_collection_id ++ str " containing all variables.") @@ -61,23 +58,22 @@ let warn_variable_shadowing = CWarnings.create ~name:"variable-shadowing" ~categ let err_redefine_all_collection () = CErrors.user_err Pp.(str "\"" ++ Id.print all_collection_id ++ str "\" is a predefined collection containing all variables. It can't be redefined.") -let process_expr env sigma fixnames e v_ty = - let variable_exists id = - try ignore (lookup_named id env); true with | Not_found -> false in +let process_expr env sigma e v_ty = + let variable_exists id = Termops.is_section_variable_env ~check:false env id in let rec aux = function | SsEmpty -> Id.Set.empty | SsType -> v_ty | SsSingl { CAst.v = id } -> set_of_id id | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) - | SsCompl e -> Id.Set.diff (full_set fixnames env) (aux e) + | SsCompl e -> Id.Set.diff (Environ.section_variables env) (aux e) | SsFwdClose e -> close_fwd env sigma (aux e) and set_of_id id = if Id.equal id all_collection_id then begin if variable_exists all_collection_id then warn_all_collection_precedence (); - full_set fixnames env + Environ.section_variables env end else if is_known_name id then begin @@ -86,24 +82,24 @@ let process_expr env sigma fixnames e v_ty = aux (CList.assoc_f Id.equal id !known_names) end else - if List.exists (Id.equal id) fixnames then - CErrors.user_err Pp.(str "Invalid recursive variable: " ++ Id.print id ++ str ".") - else if not (List.exists (NamedDecl.get_id %> Id.equal id) (named_context env)) then + if not (Environ.mem_named id env) then CErrors.user_err Pp.(str "Unknown variable: " ++ Id.print id ++ str ".") + else if not (variable_exists id) then + CErrors.user_err Pp.(Id.print id ++ str " is not a section variable.") else Id.Set.singleton id in aux e -let process_expr env sigma fixnames e ty = - let v_ty = set_of_type env sigma fixnames ty in - let s = Id.Set.union v_ty (process_expr env sigma fixnames e v_ty) in +let process_expr env sigma e ty = + let v_ty = set_of_type env sigma ty in + let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in Id.Set.elements s type t = Names.Id.Set.t -let definition_using env evd ~fixnames ~using ~terms = - let l = process_expr env evd fixnames using terms in +let definition_using env evd ~using ~terms = + let l = process_expr env evd using terms in Names.Id.Set.(CList.fold_right add l empty) let name_set id expr = @@ -154,9 +150,7 @@ let suggest_common env ppid used ids_typ skip = let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in let all_needed = really_needed env needed in - let all = List.fold_left (fun all d -> S.add (NamedDecl.get_id d) all) - S.empty (named_context env) - in + let all = Environ.section_variables env in let all = S.diff all skip in let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in let () = debug_proof_using (fun () -> diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index 5f161860fbb9..44929d4fb752 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -18,7 +18,6 @@ type t = Names.Id.Set.t val definition_using : Environ.env -> Evd.evar_map - -> fixnames:Names.Id.t list (* names of fixpoint occurring recursively, if any *) -> using:Vernacexpr.section_subset_expr -> terms:EConstr.constr list -> t From 69ea8280711a6945e3498036bd49f4823136e5c3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 9 Jun 2026 14:01:31 +0200 Subject: [PATCH 2/6] Cleanup set_used_variables We don't need to return the resulting context. --- vernac/declare.ml | 33 ++++++++++++++++----------------- vernac/declare.mli | 2 +- vernac/vernacentries.ml | 3 +-- 3 files changed, 18 insertions(+), 20 deletions(-) diff --git a/vernac/declare.ml b/vernac/declare.ml index d29422a4fb63..a4f30b86bc3b 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1981,27 +1981,26 @@ let definition_scope ps = ps.pinfo.info.scope let set_used_variables ps ~using = let open Context.Named.Declaration in + let () = if not (Option.is_empty ps.using) then + CErrors.user_err Pp.(str "Used section variables can be declared only once.") + in let env = Global.env () in - let ctx = Environ.keep_hyps env using in - let ctx_set = - List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in + let kept = Environ.really_needed env using in let vars_of = Environ.global_vars_set in - let aux env _status entry (ctx, all_safe as orig) = + (* add any letins which only depend on kept variables *) + let aux env _status entry kept = match entry with - | LocalAssum ({Context.binder_name=x},_) -> - if Id.Set.mem x all_safe then orig - else (ctx, all_safe) - | LocalDef ({Context.binder_name=x},bo, ty) as decl -> - if Id.Set.mem x all_safe then orig else + | LocalAssum ({Context.binder_name=x},_) -> kept + | LocalDef ({Context.binder_name=x},bo, ty) -> + if Id.Set.mem x kept then kept else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe - then (decl :: ctx, Id.Set.add x all_safe) - else (ctx, all_safe) in - let ctx, _ = - Environ.fold_named_context aux env ~init:(ctx,ctx_set) in - if not (Option.is_empty ps.using) then - CErrors.user_err Pp.(str "Used section variables can be declared only once"); - ctx, { ps with using = Some (Context.Named.to_vars ctx) } + if Id.Set.subset vars kept + then (Id.Set.add x kept) + else kept in + let kept = + Environ.fold_named_context aux env ~init:kept + in + { ps with using = Some kept } let interpret_proof_using pstate using = let env = Global.env () in diff --git a/vernac/declare.mli b/vernac/declare.mli index 5fbf778a6368..edf7e696f66e 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -279,7 +279,7 @@ module Proof : sig (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) *) - val set_proof_using : t -> Vernacexpr.section_subset_expr -> Constr.named_context * t + val set_proof_using : t -> Vernacexpr.section_subset_expr -> t (** Gets the set of variables declared to be used by the proof. None means no "Proof using" or #[using] was given *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 5e9b897fdea7..f5c3f1fa43b5 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2637,8 +2637,7 @@ let vernac_proof pstate tac using = 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 set_proof_using ps using = Declare.Proof.set_proof_using ps using |> snd in - let pstate = Option.fold_left set_proof_using pstate using in + let pstate = Option.fold_left Declare.Proof.set_proof_using pstate using in let pstate = Declare.Proof.finish_late_init pstate Explicit in pstate From 15f40ec5f8132936bef938d97a180d5f852a518a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 9 Jun 2026 14:52:21 +0200 Subject: [PATCH 3/6] reindent example in proof-mode.rst this example is not part of the doc for the attribute --- .../proofs/writing-proofs/proof-mode.rst | 59 ++++++++++--------- 1 file changed, 30 insertions(+), 29 deletions(-) diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 646dbaa66bc2..e21a2927b15c 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -387,48 +387,49 @@ When the proof is completed, you can exit proof mode with commands such as .. _example-print-using: - .. example :: Declaring section variables +.. example:: Declaring section variables - When a :ref:`section ` is closed with :cmd:`End`, section - variables declared with :cmd:`Proof using` are added to the theorem as - additional variables. You can see the effect on the theorem's statement - with commands such as :cmd:`Check`, :cmd:`Print` and :cmd:`About` after the - section is closed. The :cmd:`Print` and :cmd:`About` commands also show the - section variables associated with a theorem before the section is closed. + When a :ref:`section ` is closed with :cmd:`End`, section + variables declared with :cmd:`Proof using` are added to the theorem as + additional variables. You can see the effect on the theorem's statement + with commands such as :cmd:`Check`, :cmd:`Print` and :cmd:`About` after the + section is closed. The :cmd:`Print` and :cmd:`About` commands also show the + section variables associated with a theorem before the section is closed. - Adding the unnecessary section variable `radixNotZero` changes how `foo'` can be - applied. + Adding the unnecessary section variable `radixNotZero` changes how `foo'` can be + applied. - .. rocqtop:: in + .. rocqtop:: in - Section bar. - Variable radix : nat. - Hypothesis radixNotZero : 0 < radix. + Section bar. + Variable radix : nat. + Hypothesis radixNotZero : 0 < radix. - Lemma foo : 0 = 0. - Proof. reflexivity. Qed. + Lemma foo : 0 = 0. + Proof. reflexivity. Qed. - Lemma foo' : 0 = 0. - Proof using radixNotZero. reflexivity. Qed. (* radixNotZero is not needed *) + Lemma foo' : 0 = 0. + Proof using radixNotZero. reflexivity. Qed. (* radixNotZero is not needed *) - .. rocqtop:: all + .. rocqtop:: all - Print foo'. (* Doesn't show radixNotZero yet *) - End bar. - Print foo. (* Doesn't change after the End *) - Print foo'. (* "End" added type radix (used by radixNotZero) and radixNotZero *) - Goal 0 = 0. - Proof. + Print foo'. (* Doesn't show radixNotZero yet *) + End bar. - .. rocqtop:: in + Print foo. (* Doesn't change after the End *) + Print foo'. (* "End" added type radix (used by radixNotZero) and radixNotZero *) + Goal 0 = 0. + Proof. - Fail apply foo'. (* Fails because of the extra variable *) + .. rocqtop:: in - .. rocqtop:: all + Fail apply foo'. (* Fails because of the extra variable *) + + .. rocqtop:: all - apply (foo' 5). (* Can be used if the extra variable is provided explicitly *) + apply (foo' 5). (* Can be used if the extra variable is provided explicitly *) - .. rocqtop:: abort none + .. rocqtop:: abort none Proof using options ``````````````````` From 427403702e5827a72cedfc59f7d8845a07e26221 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 12 Jun 2026 15:18:54 +0200 Subject: [PATCH 4/6] add regression test --- test-suite/bugs/bug_22107_1.v | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 test-suite/bugs/bug_22107_1.v diff --git a/test-suite/bugs/bug_22107_1.v b/test-suite/bugs/bug_22107_1.v new file mode 100644 index 000000000000..767f36eb9344 --- /dev/null +++ b/test-suite/bugs/bug_22107_1.v @@ -0,0 +1,9 @@ +Goal nat -> nat. +Proof. + intros x . + epose (_:>bool). + (* questionable behaviour: unshelves a bool goal *) + unshelve eapply plus in x. + exact true. + all: exact 0. +Qed. From 4c5664fc06c2b012fbea8d3bfb9db6d1bb551d30 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 9 Jun 2026 14:52:00 +0200 Subject: [PATCH 5/6] Restore "Proof Using Clear Unused" --- .../22107-keep-using-Added.rst | 4 +++ .../proofs/writing-proofs/proof-mode.rst | 11 +++++++ proofs/proof.ml | 30 +++++++++++++++-- proofs/proof.mli | 10 ++++++ tactics/tacticErrors.ml | 11 +++++++ test-suite/bugs/bug_12608.v | 4 +-- test-suite/output/ProofUsingClear.out | 18 +++++++++++ test-suite/output/ProofUsingClear.v | 32 +++++++++++++++++++ vernac/declare.ml | 19 +++++++++-- vernac/declare.mli | 5 +-- vernac/vernacentries.ml | 2 +- 11 files changed, 136 insertions(+), 10 deletions(-) create mode 100644 doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst create mode 100644 test-suite/output/ProofUsingClear.out create mode 100644 test-suite/output/ProofUsingClear.v diff --git a/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst b/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst new file mode 100644 index 000000000000..452d2f842484 --- /dev/null +++ b/doc/changelog/08-vernac-commands-and-options/22107-keep-using-Added.rst @@ -0,0 +1,4 @@ +- **Added:** + :flag:`Proof Using Clear Unused` which automatically clears variables not allowed by a :cmd:`Proof using` annotation at the beginning of an interactive proof + (`#22107 `_, + by Gaëtan Gilbert). diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index e21a2927b15c..138bbd0ee983 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -448,6 +448,17 @@ The following options modify the behavior of ``Proof using``. invalid value will generate an error on a subsequent :cmd:`Proof` or :cmd:`Qed` command. +.. flag:: Proof Using Clear Unused + + When this :term:`flag` is on, :cmd:`Proof using` automatically + clears variables which are not allowed by the `using` expression. + +.. note:: + + When used variables are specified through :opt:`Default Proof + Using` or :attr:`using`, :flag:`Proof Using Clear Unused` only + takes effect at the :cmd:`Proof` command. If that command is left + implicit, no clearing occurs even when the flag is on. .. flag:: Suggest Proof Using diff --git a/proofs/proof.ml b/proofs/proof.ml index dde9f4d6560b..3304bbffcdc1 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -30,6 +30,7 @@ *) open Util +open Names module FocusKind = Dyn.Make() @@ -112,7 +113,7 @@ type t = (** History of the focusings, provides information on how to unfocus the proof and the extra information stored while focusing. The list is empty when the proof is fully unfocused. *) - ; name : Names.Id.t + ; name : Id.t (** the name of the theorem whose proof is being constructed *) ; poly : PolyFlags.t (** Universe polymorphism *) @@ -362,7 +363,7 @@ type data = (** Entry for the proofview *) ; stack : (Evar.t list * Evar.t list) list (** A representation of the focus stack *) - ; name : Names.Id.t + ; name : Id.t (** The name of the theorem whose proof is being constructed *) ; poly : PolyFlags.t (** Universe polymorphism *) @@ -470,3 +471,28 @@ let get_proof_context p = let purge_side_effects p = let proofview, eff = Proofview.Unsafe.purge_side_effects p.proofview in { p with proofview }, eff + +exception ProofUsingClearDependency of + Environ.env * Evd.evar_map * Id.t * Evarutil.clear_dependency_error * GlobRef.t option + +let set_used_variables env ~kept (p:t) = + let to_clear = Id.Set.diff Environ.(ids_of_named_context_val @@ named_context_val env) kept in + if Id.Set.is_empty to_clear then p + else + let entry = Proofview.initial_goals p.entry in + let err = Evarutil.OccurHypInSimpleClause None in + let tac = + Proofview.tclBIND Proofview.tclEVARMAP @@ fun sigma -> + let sigma = + List.fold_left (fun sigma (_, body, _) -> + try + Evarutil.check_and_clear_in_constr env sigma err to_clear body + with Evarutil.ClearDependencyError (id, err, gr) -> + raise (ProofUsingClearDependency (env, sigma, id, err, gr))) + sigma + entry + in + Proofview.Unsafe.tclEVARSADVANCE sigma + in + let p, _, () = run_tactic env tac p in + p diff --git a/proofs/proof.mli b/proofs/proof.mli index e1754d86acc5..c96b378c7698 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -209,3 +209,13 @@ val get_goal_context_gen : t -> int -> Evd.evar_map * Environ.env val get_proof_context : t -> Evd.evar_map * Environ.env val purge_side_effects : t -> t * Evd.side_effects + +(** [set_used_variables env kept p] clears variables not in [kept] + from the proof terms, with an error if this is impossible + (eg "#[refine]" with the refine term using a forbidden + variable). *) +val set_used_variables : Environ.env -> kept:Names.Id.Set.t -> t -> t + +(** Exposed for printing *) +exception ProofUsingClearDependency of + Environ.env * Evd.evar_map * Names.Id.t * Evarutil.clear_dependency_error * Names.GlobRef.t option diff --git a/tactics/tacticErrors.ml b/tactics/tacticErrors.ml index f179cb56941e..8088d3b5b206 100644 --- a/tactics/tacticErrors.ml +++ b/tactics/tacticErrors.ml @@ -76,6 +76,15 @@ let clear_dependency_msg env sigma id err inglobal = str "Cannot remove " ++ ppid id ++ str " as it would leave the existential " ++ Printer.pr_existential_key env sigma ev ++ str" without candidates." +let proof_using_clear_dependency_msg env sigma id err inglobal = + let msg = + match err with + | Evarutil.OccurHypInSimpleClause None -> + Id.print id ++ str " is used" ++ clear_in_global_msg inglobal ++ str " in the proof." + | _ -> clear_dependency_msg env sigma (Some id) err inglobal + in + str "Invalid \"Proof using\":" ++ spc() ++ msg + let replacing_dependency_msg env sigma id err inglobal = let pp = clear_in_global_msg inglobal in match err with @@ -118,6 +127,8 @@ exception Unhandled let tactic_interp_error_handler = function | IntroAlreadyDeclared id -> Id.print id ++ str " is already declared." + | Proof.ProofUsingClearDependency (env, sigma, id, err, inglobal) -> + proof_using_clear_dependency_msg env sigma id err inglobal | ClearDependency (env,sigma,id,err,inglobal) -> clear_dependency_msg env sigma id err inglobal | ReplacingDependency (env,sigma,id,err,inglobal) -> diff --git a/test-suite/bugs/bug_12608.v b/test-suite/bugs/bug_12608.v index 591d91c8d071..1226b9df9b09 100644 --- a/test-suite/bugs/bug_12608.v +++ b/test-suite/bugs/bug_12608.v @@ -1,3 +1,4 @@ +Set Proof Using Clear Unused. Require Import Derive. Derive A in (A = 1) as B. Proof using Type. @@ -10,8 +11,7 @@ Section S. Derive (A':nat) in nat as B'. Proof using . Unshelve. - all:exact n. - Fail Qed. + Fail all:exact n. Abort. Derive (A':nat) in nat as B'. diff --git a/test-suite/output/ProofUsingClear.out b/test-suite/output/ProofUsingClear.out new file mode 100644 index 000000000000..4d541f62d88e --- /dev/null +++ b/test-suite/output/ProofUsingClear.out @@ -0,0 +1,18 @@ +File "./output/ProofUsingClear.v", line 11, characters 15-16: +The command has indeed failed with message: +The reference y was not found in the current environment. +File "./output/ProofUsingClear.v", line 16, characters 2-19: +The command has indeed failed with message: +Invalid "Proof using": x is used in the proof. +File "./output/ProofUsingClear.v", line 18, characters 15-16: +The command has indeed failed with message: +The variable y was not found in the current environment. +1 goal + + x, y : nat + z := x + x : nat + ============================ + bar = bar +File "./output/ProofUsingClear.v", line 29, characters 2-13: +The command has indeed failed with message: +Invalid "Proof using": x is used implicitly in bar in the proof. diff --git a/test-suite/output/ProofUsingClear.v b/test-suite/output/ProofUsingClear.v new file mode 100644 index 000000000000..1624ecab8bd3 --- /dev/null +++ b/test-suite/output/ProofUsingClear.v @@ -0,0 +1,32 @@ +Set Proof Using Clear Unused. + +Section S. + + Variable x y : nat. + + Let z := x + x. + + Lemma foo : x + x = x + x. + Proof using . + Fail Check y. + exact (eq_refl z). + Defined. + + #[refine] Definition bar := x + _. + Fail Proof using. + Proof using x. + Fail exact y. + exact z. + Defined. + + Lemma baz : bar = bar. + Proof using y. (* x implicit through the type of the lemma *) + Show. + reflexivity. + Defined. + + #[refine,using="y"] Definition baz' := bar + _. + Fail Proof. + Abort. + +End S. diff --git a/vernac/declare.ml b/vernac/declare.ml index a4f30b86bc3b..3b92323ac86e 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1979,11 +1979,23 @@ let get_used_variables pf = pf.using let definition_scope ps = ps.pinfo.info.scope +let { Goptions.get = auto_clear } = + Goptions.declare_bool_option_and_ref ~key:["Proof";"Using";"Clear";"Unused"] + ~value:false + () + let set_used_variables ps ~using = let open Context.Named.Declaration in - let () = if not (Option.is_empty ps.using) then + let using = match ps.using, using with + | None, Some using -> Some using + | Some using, None -> Some using + | Some _, Some _ -> CErrors.user_err Pp.(str "Used section variables can be declared only once.") + | None, None -> None in + match using with + | None -> ps + | Some using -> let env = Global.env () in let kept = Environ.really_needed env using in let vars_of = Environ.global_vars_set in @@ -2000,7 +2012,8 @@ let set_used_variables ps ~using = let kept = Environ.fold_named_context aux env ~init:kept in - { ps with using = Some kept } + let proof = if auto_clear() then Proof.set_used_variables env ~kept ps.proof else ps.proof in + { ps with proof; using = Some kept } let interpret_proof_using pstate using = let env = Global.env () in @@ -2011,7 +2024,7 @@ let interpret_proof_using pstate using = Proof_using.definition_using env sigma ~using ~terms let set_proof_using pstate using = - let using = interpret_proof_using pstate using in + let using = Option.map (interpret_proof_using pstate) using in set_used_variables pstate ~using let get_open_goals ps = diff --git a/vernac/declare.mli b/vernac/declare.mli index edf7e696f66e..b72e14ce7fc4 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -278,8 +278,9 @@ module Proof : sig 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_proof_using : t -> Vernacexpr.section_subset_expr -> t + (w.r.t. type dependencies and let-ins covered by it). + With [None], get the variables from the "using" attribute. *) + val set_proof_using : t -> Vernacexpr.section_subset_expr option -> t (** Gets the set of variables declared to be used by the proof. None means no "Proof using" or #[using] was given *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f5c3f1fa43b5..b9b2bf658079 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2637,7 +2637,7 @@ let vernac_proof pstate tac using = 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 Declare.Proof.set_proof_using pstate using in + let pstate = Declare.Proof.set_proof_using pstate using in let pstate = Declare.Proof.finish_late_init pstate Explicit in pstate From 2e63732547656ff14a6b3e7847f142e200829667 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 10 Jun 2026 15:12:51 +0200 Subject: [PATCH 6/6] overlay --- dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh | 1 + 1 file changed, 1 insertion(+) create mode 100644 dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh diff --git a/dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh b/dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh new file mode 100644 index 000000000000..47336c70fb99 --- /dev/null +++ b/dev/ci/user-overlays/22107-SkySkimmer-keep-using.sh @@ -0,0 +1 @@ +overlay vsrocq https://github.com/SkySkimmer/vsrocq keep-using 22107