From 980c7ea217428b0f472a53abf1df747a3d7b0f98 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 30 Apr 2026 14:43:05 +0200 Subject: [PATCH 01/17] Keep track of variable status (secvar or not) in named contexts Close #6773 --- doc/plugin_tutorial/tuto3/src/tuto_tactic.ml | 4 +- engine/eConstr.ml | 30 ++++- engine/eConstr.mli | 21 +++- engine/evarutil.ml | 28 ++--- engine/evarutil.mli | 1 - engine/evd.ml | 14 +-- engine/proofview.ml | 22 ++-- engine/termops.ml | 24 ++-- ide/rocqide/idetop.ml | 2 +- interp/constrintern.ml | 2 +- kernel/environ.ml | 110 ++++++++++++------ kernel/environ.mli | 29 +++-- kernel/safe_typing.ml | 2 +- kernel/typeops.ml | 1 + plugins/cc/ccalgo.ml | 2 +- plugins/derive/derive.ml | 6 +- plugins/extraction/extraction.ml | 6 +- plugins/funind/functional_principles_types.ml | 2 +- plugins/funind/gen_principle.ml | 2 +- plugins/funind/glob_term_to_relation.ml | 14 +-- plugins/funind/recdef.ml | 5 +- plugins/ltac/leminv.ml | 12 +- plugins/ltac2/tac2core.ml | 2 +- plugins/micromega/zify.ml | 4 +- plugins/ssr/ssrcommon.ml | 8 +- plugins/ssr/ssripats.ml | 6 +- plugins/ssrmatching/ssrmatching.ml | 2 +- pretyping/evarconv.ml | 2 +- pretyping/evardefine.ml | 4 +- pretyping/evarsolve.ml | 2 +- pretyping/heads.ml | 2 +- pretyping/unification.ml | 14 +-- printing/printer.ml | 2 +- proofs/logic.ml | 88 +++++++------- proofs/logic.mli | 2 +- proofs/refine.ml | 42 ++++--- proofs/subproof.ml | 2 +- proofs/tacmach.ml | 7 +- tactics/abstract.ml | 26 +---- tactics/class_tactics.ml | 10 +- tactics/equality.ml | 4 +- tactics/fixTactics.ml | 4 +- tactics/induction.ml | 15 ++- tactics/rewrite.ml | 6 +- tactics/tactics.ml | 39 ++++--- test-suite/bugs/bug_6773.v | 14 +++ vernac/comFixpoint.ml | 4 +- vernac/declare.ml | 16 ++- vernac/retrieveObl.ml | 2 + 49 files changed, 384 insertions(+), 284 deletions(-) create mode 100644 test-suite/bugs/bug_6773.v diff --git a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml index 30c08dee43c5..6fa5f8080d87 100644 --- a/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml +++ b/doc/plugin_tutorial/tuto3/src/tuto_tactic.ml @@ -102,8 +102,8 @@ let two_lambda_pattern sigma term = function like *) let get_type_of_hyp env id = match EConstr.lookup_named id env with - | Context.Named.Declaration.LocalAssum (_, ty) -> ty - | _ -> CErrors.user_err (let open Pp in + | LocalAssum (_, ty) -> ty + | LocalDef _ -> CErrors.user_err (let open Pp in str (Names.Id.to_string id) ++ str " is not a plain hypothesis") diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 60054cd04ddd..c1b629fbc274 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1220,16 +1220,25 @@ let destArity sigma = let push_rel d e = push_rel (cast_rel_decl unsafe_eq unsafe_relevance_eq d) e let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq unsafe_relevance_eq d) e let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq unsafe_relevance_eq d) e -let push_named d e = push_named (cast_named_decl unsafe_eq unsafe_relevance_eq d) e -let push_named_context d e = push_named_context (cast_named_context unsafe_eq unsafe_relevance_eq d) e -let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq unsafe_relevance_eq d) e +let push_named status d e = push_named status (cast_named_decl unsafe_eq unsafe_relevance_eq d) e +let push_named_context d e = + List.fold_right (fun (status, d) env -> push_named status d env) d e +let push_named_context_val status d e = push_named_context_val status (cast_named_decl unsafe_eq unsafe_relevance_eq d) e let rel_context e = cast_rel_context (sym unsafe_eq) (sym unsafe_relevance_eq) (rel_context e) let named_context e = cast_named_context (sym unsafe_eq) (sym unsafe_relevance_eq) (named_context e) -let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq unsafe_relevance_eq e) +let val_of_named_context ctxt = + List.fold_right (fun (status,d) ctxt -> push_named_context_val status d ctxt) + ctxt Environ.empty_named_context_val + let named_context_of_val e = cast_named_context (sym unsafe_eq) (sym unsafe_relevance_eq) (named_context_of_val e) +let named_context_of_val_with_status + : named_context_val -> (var_status * named_declaration) list = + let Refl, Refl = unsafe_eq, unsafe_relevance_eq in + named_context_of_val_with_status + let of_existential : Constr.existential -> existential = let gen : type a b. (a,b) eq -> 'c * b SList.t -> 'c * a SList.t = fun Refl x -> x in gen unsafe_eq @@ -1248,10 +1257,21 @@ let map_rel_context_in_env f env sign = aux env [] (List.rev sign) let match_named_context_val : - named_context_val -> (named_declaration * named_context_val) option = + named_context_val -> (var_status * named_declaration * named_context_val) option = match unsafe_eq, unsafe_relevance_eq with | Refl, Refl -> match_named_context_val +let fold_named_context : + (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a = + let Refl, Refl = unsafe_eq, unsafe_relevance_eq in + Environ.fold_named_context + +let map_named_val : + (var_status -> named_declaration -> var_status * named_declaration) -> + named_context_val -> named_context_val = + match unsafe_eq, unsafe_relevance_eq with + | Refl, Refl -> map_named_val + let identity_subst_val : named_context_val -> t SList.t = fun ctx -> SList.defaultn (List.length ctx.Environ.env_named_ctx) SList.empty diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 861bdf094d96..0b7cec293478 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -424,15 +424,19 @@ val push_rel : rel_declaration -> env -> env val push_rel_context : rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env -val push_named : named_declaration -> env -> env -val push_named_context : named_context -> env -> env -val push_named_context_val : named_declaration -> named_context_val -> named_context_val +val push_named : var_status -> named_declaration -> env -> env +val push_named_context : (var_status * named_declaration) list -> env -> env +val push_named_context_val : var_status -> named_declaration -> named_context_val -> named_context_val val rel_context : env -> rel_context val named_context : env -> named_context -val val_of_named_context : named_context -> named_context_val +val val_of_named_context : (var_status * named_declaration) list -> named_context_val val named_context_of_val : named_context_val -> named_context +val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list + +val fold_named_context : + (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a val lookup_rel : int -> env -> rel_declaration val lookup_named : variable -> env -> named_declaration @@ -445,7 +449,14 @@ val map_rel_context_in_env : (env -> constr -> constr) -> env -> rel_context -> rel_context val match_named_context_val : - named_context_val -> (named_declaration * named_context_val) option + named_context_val -> (var_status * named_declaration * named_context_val) option + +(** [map_named_val f ctxt] apply [f] to the body and the type of + each declarations. + *** /!\ *** [f t] must preserve the name *) +val map_named_val : + (var_status -> named_declaration -> var_status * named_declaration) -> + named_context_val -> named_context_val val identity_subst_val : named_context_val -> t SList.t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 438e23bd16b5..aa451c09b682 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -63,17 +63,17 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} = let nf_relevance sigma r = UState.nf_relevance (Evd.ustate sigma) r -let nf_named_context_evar sigma ctx = - Context.Named.map_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx +let nf_named_decl_evar sigma status ctx = + status, Context.Named.Declaration.map_constr_with_relevance (nf_relevance sigma) (nf_evars_universes sigma) ctx let nf_rel_context_evar sigma ctx = let nf_relevance r = ERelevance.make (ERelevance.kind sigma r) in Context.Rel.map_with_relevance nf_relevance (nf_evar sigma) ctx let nf_env_evar sigma env = - let nc' = nf_named_context_evar sigma (Environ.named_context env) in + let nc' = Environ.map_named_val (nf_named_decl_evar sigma) (Environ.named_context_val env) in let rel' = nf_rel_context_evar sigma (EConstr.rel_context env) in - EConstr.push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env) + EConstr.push_rel_context rel' (reset_with_named_context nc' env) let nf_evar_info evc info = map_evar_info (nf_evar evc) info @@ -114,6 +114,7 @@ let is_ground_env evd env = | RelDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b) | _ -> true in let is_ground_named_decl = function + (* skip if SecVar? *) | NamedDecl.LocalDef (_,b,_) -> is_ground_term evd (EConstr.of_constr b) | _ -> true in List.for_all is_ground_rel_decl (rel_context env) && @@ -303,14 +304,15 @@ let push_rel_decl_to_named_context in let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with | None -> empty_named_context_val - | Some (decl, nc) -> + | Some (status, decl, nc) -> if Id.equal id0 (NamedDecl.get_id decl) then - (* Stop here, the variable cannot occur before its definition *) - push_named_context_val (NamedDecl.set_id id decl) nc + (* Stop here, the variable cannot occur before its definition + NB: we lose section variable status *) + push_named_context_val ProofVar (NamedDecl.set_id id decl) nc else let nc = replace_var_named_declaration id0 id nc in let vsubst = [id0 , mkVar id] in - push_named_context_val (map_decl (fun c -> replace_vars sigma vsubst c) decl) nc + push_named_context_val status (map_decl (fun c -> replace_vars sigma vsubst c) decl) nc in let extract_if_neq id = function | Anonymous -> None @@ -333,7 +335,7 @@ let push_rel_decl_to_named_context let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in { ext_subst = push_var id ext.ext_subst; ext_avoid = Id.Set.add id ext.ext_avoid; - ext_ctx = push_named_context_val d ext.ext_ctx } + ext_ctx = push_named_context_val ProofVar d ext.ext_ctx } else (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given @@ -345,12 +347,12 @@ let push_rel_decl_to_named_context let avoid = Id.Set.add id (Id.Set.add id0 ext.ext_avoid) in { ext_subst = push_var id0 subst; ext_avoid = avoid; - ext_ctx = push_named_context_val d nc } + ext_ctx = push_named_context_val ProofVar d nc } | None -> let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst sigma ext.ext_subst) in { ext_subst = push_var id ext.ext_subst; ext_avoid = Id.Set.add id ext.ext_avoid; - ext_ctx = push_named_context_val d ext.ext_ctx } + ext_ctx = push_named_context_val ProofVar d ext.ext_ctx } let csubst_instance subst ctx = let fold decl accu = match Id.Map.find (NamedDecl.get_id decl) subst.csubst_rev with @@ -609,10 +611,10 @@ let clear_hyps_in_evi_main env sigma hyps terms ids = let terms = List.map (check_and_clear_in_constr ~is_section_variable env evdref (OccurHypInSimpleClause None) ids ~global) terms in let nhyps = - let check_context decl = + let check_context status decl = let decl = EConstr.of_named_decl decl in let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in - EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) decl + status, EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) decl in remove_hyps ids check_context hyps in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index dcd6036b5b1c..75f9ac93240b 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -128,7 +128,6 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env diff --git a/engine/evd.ml b/engine/evd.ml index 8a79608a92a9..87f913f0dfc9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -257,15 +257,15 @@ let evar_hyps evi = evi.evar_hyps let evar_filtered_hyps evi = match Filter.repr (evar_filter evi) with | None -> evar_hyps evi | Some filter -> - let rec make_hyps filter ctxt = match filter, ctxt with - | [], [] -> empty_named_context_val - | false :: filter, _ :: ctxt -> make_hyps filter ctxt - | true :: filter, decl :: ctxt -> + let rec make_hyps filter ctxt = match filter, match_named_context_val ctxt with + | [], None -> empty_named_context_val + | false :: filter, Some (_, _, ctxt) -> make_hyps filter ctxt + | true :: filter, Some (status, decl, ctxt) -> let hyps = make_hyps filter ctxt in - push_named_context_val decl hyps + push_named_context_val status decl hyps | _ -> instance_mismatch () in - make_hyps filter (evar_context evi) + make_hyps filter (evar_hyps evi) let evar_env env evi = Environ.reset_with_named_context evi.evar_hyps env @@ -290,7 +290,7 @@ let map_when_undefined (type a b) f : (a, b) when_undefined -> (a, b) when_undef let map_evar_info f evi = {evi with evar_body = map_evar_body f evi.evar_body; - evar_hyps = map_named_val (fun d -> NamedDecl.map_constr f d) evi.evar_hyps; + evar_hyps = map_named_val (fun status d -> status, NamedDecl.map_constr f d) evi.evar_hyps; evar_concl = map_when_undefined f evi.evar_concl; evar_candidates = map_when_undefined (fun c -> Option.map (List.map f) c) evi.evar_candidates } diff --git a/engine/proofview.ml b/engine/proofview.ml index 10e28d719656..60e00a223312 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -41,7 +41,7 @@ let proofview p = let compact el ({ solution } as pv) = let nf c = Evarutil.nf_evar solution c in let nf0 c = EConstr.(to_constr ~abort_on_undefined_evars:false solution (of_constr c)) in - let nf_hyps hyps = Environ.map_named_val (fun d -> map_constr nf0 d) hyps in + let nf_hyps hyps = Environ.map_named_val (fun status d -> status, map_constr nf0 d) hyps in let size = Evd.fold (fun _ _ i -> i+1) solution 0 in let new_el = List.map (fun (hyps,t,ty) -> nf_hyps hyps, nf t, nf ty) el in let pruned_solution = Evd.drop_all_defined solution in @@ -916,15 +916,19 @@ module Progress = struct let eq_named_context_val sigma1 sigma2 ctx1 ctx2 = let r_eq _ _ = true (* ignore relevances *) in let c1 = EConstr.named_context_of_val ctx1 and c2 = EConstr.named_context_of_val ctx2 in + (* should we check variable status? if x is secvar, + [rename x into x'; rename x' into x] loses the secvar status + so maybe should progress? + NB Don't forget to also change the fast path if we change this *) let eq_named_declaration d1 d2 = match d1, d2 with | LocalAssum (i1,t1), LocalAssum (i2,t2) -> - Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 t1 t2 + Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 t1 t2 | LocalDef (i1,c1,t1), LocalDef (i2,c2,t2) -> - Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 c1 c2 - && eq_constr sigma1 sigma2 t1 t2 + Context.eq_annot Names.Id.equal r_eq i1 i2 && eq_constr sigma1 sigma2 c1 c2 && + eq_constr sigma1 sigma2 t1 t2 | _ -> - false + false in (* NB: can't use List.equal because it shortcuts on physical equality *) List.for_all2eq eq_named_declaration c1 c2 @@ -960,9 +964,11 @@ module Progress = struct let c1 = EConstr.named_context_of_val ctx1 in let c2 = EConstr.named_context_of_val ctx2 in let eq_named_declaration d1 d2 = match d1, d2 with - | LocalAssum (i1, _), LocalAssum (i2, _) -> Context.eq_annot Names.Id.equal r_eq i1 i2 - | LocalDef (i1, _, _), LocalDef (i2, _, _) -> Context.eq_annot Names.Id.equal r_eq i1 i2 - | _ -> false + | LocalAssum (i1, _), LocalAssum (i2, _) -> + Context.eq_annot Names.Id.equal r_eq i1 i2 + | LocalDef (i1, _, _), LocalDef (i2, _, _) -> + Context.eq_annot Names.Id.equal r_eq i1 i2 + | _ -> false in List.for_all2eq eq_named_declaration c1 c2 diff --git a/engine/termops.ml b/engine/termops.ml index 660e57c349df..ad1f64cf9deb 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -62,7 +62,7 @@ module Internal = struct let print_named_context env sigma = hv 0 (fold_named_context - (fun env d pps -> + (fun env _status d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) env ~init:(mt ())) @@ -74,7 +74,7 @@ module Internal = struct let print_env env sigma = let sign_env = fold_named_context - (fun env d pps -> + (fun env _status d pps -> let pidt = pr_var_decl env sigma d in (pps ++ fnl () ++ pidt)) env ~init:(mt ()) @@ -149,9 +149,11 @@ let pr_decl env sigma (decl,ok) = let open NamedDecl in let print_constr = Internal.print_kconstr in match decl with - | LocalAssum ({binder_name=id},_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") - | LocalDef ({binder_name=id},c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ - print_constr env sigma c ++ str (if ok then ")" else "}") + | LocalAssum ({binder_name=id},_) -> + if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") + | LocalDef ({binder_name=id},c,_) -> + str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ + print_constr env sigma c ++ str (if ok then ")" else "}") let pr_evar_source env sigma = function | Evar_kinds.NamedHole id -> Id.print id @@ -877,10 +879,7 @@ let dependent sigma c t = dependent_main false sigma c t let dependent_no_evar sigma c t = dependent_main true sigma c t let dependent_in_decl sigma a decl = - let open NamedDecl in - match decl with - | LocalAssum (_,t) -> dependent sigma a t - | LocalDef (_, body, t) -> dependent sigma a body || dependent sigma a t + NamedDecl.exists (dependent sigma a) decl let count_occurrences sigma m t = let open EConstr in @@ -1008,6 +1007,7 @@ let ids_of_context env = let names_of_rel_context env = List.map RelDecl.get_name (rel_context env) +(* XXX use var status (NOT IN THIS ENV) *) let is_section_variable env id = try let _ = Environ.lookup_named id env in true with Not_found -> false @@ -1203,9 +1203,9 @@ let compact_named_context sigma sign = let clear_named_body id env = let open NamedDecl in - let aux _ = function - | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named (LocalAssum (id',t)) - | d -> push_named d in + let aux _ status = function + | LocalDef (id',c,t) when Id.equal id id'.binder_name -> push_named status (LocalAssum (id',t)) + | d -> push_named status d in fold_named_context aux env ~init:(reset_context env) let global_vars_set env sigma constr = diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml index 0336f939ceba..726b1a6f1e76 100644 --- a/ide/rocqide/idetop.ml +++ b/ide/rocqide/idetop.ml @@ -301,7 +301,7 @@ let hints () = | [] -> None | g :: _ -> let env = Evd.evar_filtered_env (Global.env ()) (Evd.find_undefined sigma g) in - let get_hint_hyp env d accu = hyp_next_tac sigma env d :: accu in + let get_hint_hyp env _ d accu = hyp_next_tac sigma env d :: accu in let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in Some (hint_hyps, concl_next_tac) with Vernacstate.Declare.NoCurrentProof -> None diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 35ff54ca4669..3696fb418ac1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -3110,7 +3110,7 @@ let interp_context_evars_gen ?(program_mode=false) ?(unconstrained_sorts = false let interp_named_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable env sigma bl = let extract_name ?loc = function Name id -> id | Anonymous -> user_err ?loc Pp.(str "Unexpected anonymous variable.") in let make_decl ?loc = Context.Named.Declaration.of_rel_decl (extract_name ?loc) in - interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable ~dump:false env sigma make_decl EConstr.push_named bl + interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ?autoimp_enable ~dump:false env sigma make_decl (EConstr.push_named ProofVar) bl let interp_context_evars ?program_mode ?unconstrained_sorts ?poly ?impl_env env sigma bl = interp_context_evars_gen ?program_mode ?unconstrained_sorts ?poly ?impl_env ~autoimp_enable:false ~dump:true env sigma (fun ?loc d -> d) EConstr.push_rel bl diff --git a/kernel/environ.ml b/kernel/environ.ml index 54d4ded25492..850bfe73e9e7 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -80,6 +80,7 @@ type named_context_val = { env_named_ctx : Constr.named_context; env_named_map : Constr.named_declaration Id.Map.t; env_named_idx : Constr.named_declaration Range.t; + env_named_secvars : Id.Set.t; } type rel_context_val = { @@ -118,6 +119,7 @@ let empty_named_context_val = { env_named_ctx = []; env_named_map = Id.Map.empty; env_named_idx = Range.empty; + env_named_secvars = Id.Set.empty; } let empty_rel_context_val = { @@ -187,43 +189,78 @@ let set_rel_context_val v env = env_nb_rel = Range.length v.env_rel_map; } (* Named context *) - -let push_named_context_val d ctxt = -(* assert (not (Id.Map.mem (NamedDecl.get_id d) ctxt.env_named_map)); *) +type var_status = SecVar | ProofVar + +let push_named_context_val status d ctxt = + let id = NamedDecl.get_id d in + (* assert (not (Id.Map.mem id ctxt.env_named_map)); *) + let secvars = match status with + | ProofVar -> ctxt.env_named_secvars + | SecVar -> Id.Set.add id ctxt.env_named_secvars + in { env_named_ctx = Context.Named.add d ctxt.env_named_ctx; - env_named_map = Id.Map.add (NamedDecl.get_id d) d ctxt.env_named_map; + env_named_map = Id.Map.add id d ctxt.env_named_map; env_named_idx = Range.cons d ctxt.env_named_idx; + env_named_secvars = secvars; } +let var_status_ctxt ?(check=true) id ctxt = + if Id.Set.mem id ctxt.env_named_secvars then SecVar + else + let () = assert (not check || Id.Map.mem id ctxt.env_named_map) in + ProofVar + +let var_status ?check id env = var_status_ctxt ?check id env.env_named_context + let match_named_context_val c = match c.env_named_ctx with | [] -> None | decl :: ctx -> - let map = Id.Map.remove (NamedDecl.get_id decl) c.env_named_map in - let cval = { env_named_ctx = ctx; env_named_map = map; env_named_idx = Range.tl c.env_named_idx } in - Some (decl, cval) + let id = NamedDecl.get_id decl in + let map = Id.Map.remove id c.env_named_map in + let secvars = Id.Set.remove id c.env_named_secvars in + let status = if secvars == c.env_named_secvars then ProofVar else SecVar in + let cval = { + env_named_ctx = ctx; + env_named_map = map; + env_named_idx = Range.tl c.env_named_idx; + env_named_secvars = secvars; + } + in + Some (status, decl, cval) let map_named_val f ctxt = let open Context.Named.Declaration in - let fold accu d = - let d' = f d in - let accu = - if d == d' then accu - else Id.Map.set (get_id d) d' accu + let fold (map,secvars) d = + let id = get_id d in + let status = var_status_ctxt ~check:false id ctxt in + let status', d' = f status d in + let () = assert (Id.equal id (get_id d')) in + let map = + if d == d' then map + else Id.Map.set id d' map + in + let secvars = + if status == status' then secvars else + match status' with + | SecVar -> Id.Set.add id secvars + | ProofVar -> Id.Set.remove id secvars in - (accu, d') + ((map,secvars), d') in - let map, ctx = List.Smart.fold_left_map fold ctxt.env_named_map ctxt.env_named_ctx in - if map == ctxt.env_named_map then ctxt + let (map,secvars), ctx = List.Smart.fold_left_map fold (ctxt.env_named_map,ctxt.env_named_secvars) ctxt.env_named_ctx in + if map == ctxt.env_named_map && secvars == ctxt.env_named_secvars then ctxt else let idx = List.fold_right Range.cons ctx Range.empty in - { env_named_ctx = ctx; env_named_map = map; env_named_idx = idx } + { env_named_ctx = ctx; env_named_map = map; env_named_idx = idx; env_named_secvars = secvars } + +let push_named status d env = + {env with env_named_context = push_named_context_val status d env.env_named_context} -let push_named d env = - {env with env_named_context = push_named_context_val d env.env_named_context} +let mem_named_ctxt id ctxt = + Id.Map.mem id ctxt.env_named_map -let mem_named id env = - Id.Map.mem id env.env_named_context.env_named_map +let mem_named id env = mem_named_ctxt id env.env_named_context let lookup_named id env = Id.Map.find id env.env_named_context.env_named_map @@ -430,14 +467,18 @@ let fold_rel_context f env ~init = let named_context_of_val c = c.env_named_ctx +let named_context_of_val_with_status c = + List.map (fun d -> var_status_ctxt ~check:false (NamedDecl.get_id d) c, d) c.env_named_ctx + let ids_of_named_context_val c = Id.Map.domain c.env_named_map let empty_named_context = Context.Named.empty -let push_named_context = List.fold_right push_named +let push_named_context = List.fold_right (fun (status,d) env -> push_named status d env) let val_of_named_context ctxt = - List.fold_right push_named_context_val ctxt empty_named_context_val + List.fold_right (fun (status,d) ctxt -> push_named_context_val status d ctxt) + ctxt empty_named_context_val let eq_named_context_val c1 c2 = @@ -482,10 +523,10 @@ let fold_named_context f env ~init = let rec fold_right env = match match_named_context_val env.env_named_context with | None -> init - | Some (d, rem) -> + | Some (status, d, rem) -> let env = reset_with_named_context rem env in - f env d (fold_right env) + f env status d (fold_right env) in fold_right env let fold_named_context_reverse f ~init env = @@ -1017,12 +1058,13 @@ let apply_to_hyp ctxt id f = let open Context.Named.Declaration in let rec aux rtail ctxt = match match_named_context_val ctxt with - | Some (d, ctxt) -> - if Id.equal (get_id d) id then - push_named_context_val (f ctxt.env_named_ctx d rtail) ctxt - else - let ctxt' = aux (d::rtail) ctxt in - push_named_context_val d ctxt' + | Some (status, d, ctxt) -> + if Id.equal (get_id d) id then + let status, d' = f ctxt.env_named_ctx status d rtail in + push_named_context_val status d' ctxt + else + let ctxt' = aux (d::rtail) ctxt in + push_named_context_val status d ctxt' | None -> raise Hyp_not_found in aux [] ctxt @@ -1032,7 +1074,7 @@ let remove_hyps ids check_context ctxt = if Id.Set.is_empty ids then ctxt, false else match match_named_context_val ctxt with | None -> empty_named_context_val, false - | Some (d, rctxt) -> + | Some (status, d, rctxt) -> let id0 = Context.Named.Declaration.get_id d in let removed = Id.Set.mem id0 ids in let ids = if removed then Id.Set.remove id0 ids else ids in @@ -1041,10 +1083,10 @@ let remove_hyps ids check_context ctxt = else if not seen then ctxt, false else let rctxt' = ans in - let d' = check_context d in - if d == d' && rctxt == rctxt' then + let status', d' = check_context status d in + if status == status' && d == d' && rctxt == rctxt' then ctxt, true - else push_named_context_val d' rctxt', true + else push_named_context_val status' d' rctxt', true in fst (remove_hyps ids ctxt) diff --git a/kernel/environ.mli b/kernel/environ.mli index 58c43725e226..477652dc15f5 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -43,6 +43,7 @@ type named_context_val = private { (** Identifier-indexed version of [env_named_ctx] *) env_named_idx : Constr.named_declaration Range.t; (** Same as env_named_ctx but with a fast-access list. *) + env_named_secvars : Id.Set.t; } type rel_context_val = private { @@ -110,24 +111,32 @@ val fold_rel_context : (** {5 Context of variables (section variables and goal assumptions) } *) +type var_status = SecVar | ProofVar + +val var_status_ctxt : ?check:bool -> Id.t -> named_context_val -> var_status +val var_status : ?check:bool -> Id.t -> env -> var_status + val named_context_of_val : named_context_val -> Constr.named_context -val val_of_named_context : Constr.named_context -> named_context_val +val val_of_named_context : (var_status * Constr.named_declaration) list -> named_context_val val empty_named_context_val : named_context_val val ids_of_named_context_val : named_context_val -> Id.Set.t +val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list (** [map_named_val f ctxt] apply [f] to the body and the type of each declarations. - *** /!\ *** [f t] should be convertible with t, and preserve the name *) + *** /!\ *** [f t] must preserve the name *) val map_named_val : - (named_declaration -> named_declaration) -> named_context_val -> named_context_val + (var_status -> named_declaration -> var_status * named_declaration) -> + named_context_val -> named_context_val -val push_named : Constr.named_declaration -> env -> env -val push_named_context : Constr.named_context -> env -> env +val push_named : var_status -> Constr.named_declaration -> env -> env +val push_named_context : (var_status * Constr.named_declaration) list -> env -> env val push_named_context_val : - Constr.named_declaration -> named_context_val -> named_context_val + var_status -> Constr.named_declaration -> named_context_val -> named_context_val +val mem_named_ctxt : variable -> named_context_val -> bool val mem_named : variable -> env -> bool (** Looks up in the context of local vars referred by names ([named_context]) @@ -142,9 +151,9 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : - (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> var_status -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -val match_named_context_val : named_context_val -> (named_declaration * named_context_val) option +val match_named_context_val : named_context_val -> (var_status * named_declaration * named_context_val) option (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : @@ -470,10 +479,10 @@ exception Hyp_not_found return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) val apply_to_hyp : named_context_val -> variable -> - (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) -> + (Constr.named_context -> var_status -> Constr.named_declaration -> Constr.named_context -> var_status * Constr.named_declaration) -> named_context_val -val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (var_status -> Constr.named_declaration -> var_status * Constr.named_declaration) -> named_context_val -> named_context_val val is_polymorphic : env -> Names.GlobRef.t -> bool val is_template_polymorphic : env -> GlobRef.t -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index c91523b7cc6a..4e285f1d5d25 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -735,7 +735,7 @@ let safe_push_named d env = let _ = Environ.lookup_named id env in CErrors.user_err Pp.(pr_sequence str ["Identifier"; Id.to_string id; "already defined."]) with Not_found -> () in - Environ.push_named d env + Environ.push_named SecVar d env let push_named_def (id,de) senv = let sections = get_section senv.sections in diff --git a/kernel/typeops.ml b/kernel/typeops.ml index cef4fa076b0c..6aebeaeae274 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -172,6 +172,7 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) +(* TODO use var status instead *) let check_hyps_inclusion env ?evars c sign = let conv env a b = conv env ?evars a b in Context.Named.fold_outside diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 3724149b3c1f..37187f2f930f 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -895,7 +895,7 @@ let new_state_var typ state = let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in let id = Namegen.next_ident_away __eps__ ids in let r = EConstr.ERelevance.relevant in (* TODO relevance *) - state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env; + state.env<- EConstr.push_named ProofVar (Context.Named.Declaration.LocalAssum (make_annot id r,typ)) state.env; id let complete_one_class state i= diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 68e9d6e99aeb..a56278ad75dd 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -31,10 +31,10 @@ let rec fill_assumptions env sigma = function ~typeclass_candidate:false t in let decl = LocalDef (na,ev,t) in - let sigma, env, ctx = fill_assumptions (EConstr.push_named decl env) sigma ctx in + let sigma, env, ctx = fill_assumptions (EConstr.push_named ProofVar decl env) sigma ctx in sigma, env, decl :: ctx | LocalDef _ as decl :: ctx -> - let sigma, env, ctx = fill_assumptions (EConstr.push_named decl env) sigma ctx in + let sigma, env, ctx = fill_assumptions (EConstr.push_named ProofVar decl env) sigma ctx in sigma, env, decl :: ctx (** [start_deriving f suchthat lemma] starts a proof of [suchthat] @@ -70,7 +70,7 @@ let start_deriving ~atts bl suchthat name : Declare.Proof.t = | LocalDef (id, c, t) as d :: ctx -> TCons ( env , sigma , t , (fun sigma ef' -> let sigma = Evd.define (fst (EConstr.destEvar sigma ef')) c sigma in - aux (EConstr.push_named d env) sigma ctx)) in + aux (EConstr.push_named ProofVar d env) sigma ctx)) in aux env sigma ctx' in let kind = Decls.(IsDefinition Definition) in let info = Declare.Info.make ~poly ~kind () in diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 4d9dac9c8fac..697be94d02a8 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -748,11 +748,7 @@ let rec extract_term table env sg mle mlt c args = | Evar _ | Meta _ -> MLaxiom "evar" | Var v -> (* Only during Show Extraction *) - let open Context.Named.Declaration in - let ty = match EConstr.lookup_named v env with - | LocalAssum (_,ty) -> ty - | LocalDef (_,_,ty) -> ty - in + let ty = Context.Named.Declaration.get_type @@ EConstr.lookup_named v env in let vty = extract_type table env sg [] 0 ty [] in let r = { glob = GlobRef.VarRef v; inst = InfvInst.empty } in let extract_var mlt = put_magic (mlt,vty) (MLglob r) in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 8cc89c153d3c..138548108a0d 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -73,7 +73,7 @@ let compute_new_princ_type_from_rel env rel_to_fun sorts princ_type = List.map_i change_predicate_sort 0 princ_type_info.predicates in let env_with_params_and_predicates = - List.fold_right Environ.push_named new_predicates env_with_params + List.fold_right (Environ.push_named ProofVar) new_predicates env_with_params in let rel_as_kn = fst diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 04a8ece16bfd..9806eea7b056 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -54,7 +54,7 @@ let build_newrecursive lnameargsardef = let open Context.Named.Declaration in let r = ERelevance.relevant in (* TODO relevance *) - ( EConstr.push_named + ( EConstr.push_named ProofVar (LocalAssum (Context.make_annot recname r, arity)) env , Id.Map.add recname impl impls )) diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6793af714b96..0138c0d71c03 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -310,8 +310,8 @@ let raw_push_named (na, raw_value, raw_typ) env = let na = make_annot id ERelevance.relevant in (* TODO relevance *) match raw_value with - | None -> EConstr.push_named (NamedDecl.LocalAssum (na, typ)) env - | Some value -> EConstr.push_named (NamedDecl.LocalDef (na, value, typ)) env + | None -> EConstr.push_named ProofVar (NamedDecl.LocalAssum (na, typ)) env + | Some value -> EConstr.push_named ProofVar (NamedDecl.LocalDef (na, value, typ)) env ) let add_pat_variables sigma pat typ env : Environ.env = @@ -362,7 +362,7 @@ let add_pat_variables sigma pat typ env : Environ.env = ++ Printer.pr_lconstr_env env sigma new_t ++ fnl () ); let open Context.Named.Declaration in - (Environ.push_named (LocalAssum (na, new_t)) env, mkVar id :: ctxt) + (Environ.push_named ProofVar (LocalAssum (na, new_t)) env, mkVar id :: ctxt) | LocalDef (({binder_name = Name id} as na), v, t) -> let na = {na with binder_name = id} in let new_t = substl ctxt t in @@ -379,7 +379,7 @@ let add_pat_variables sigma pat typ env : Environ.env = ++ Printer.pr_lconstr_env env sigma new_v ++ fnl () ); let open Context.Named.Declaration in - ( Environ.push_named (LocalDef (na, new_v, new_t)) env + ( Environ.push_named ProofVar (LocalDef (na, new_v, new_t)) env , mkVar id :: ctxt )) (Environ.rel_context new_env) ~init:(env, [])) @@ -643,7 +643,7 @@ let rec build_entry_lc env sigma funnames avoid rt : match n with | Anonymous -> env | Name id -> - EConstr.push_named + EConstr.push_named ProofVar (NamedDecl.LocalDef (make_annot id v_r, v_as_constr, v_type)) env in @@ -1318,7 +1318,7 @@ let do_build_inductive evd (funconstants : pconstant list) let u = EConstr.EInstance.make u in let evd, t = Typing.type_of env evd (EConstr.mkConstU (c, u)) in ( evd - , EConstr.push_named (LocalAssum (make_annot id ERelevance.relevant, t)) env + , EConstr.push_named ProofVar (LocalAssum (make_annot id ERelevance.relevant, t)) env )) funnames (Array.of_list funconstants) @@ -1379,7 +1379,7 @@ let do_build_inductive evd (funconstants : pconstant list) in let r = ERelevance.relevant in (* TODO relevance *) - EConstr.push_named (LocalAssum (make_annot rel_name r, rex)) env) + EConstr.push_named ProofVar (LocalAssum (make_annot rel_name r, rex)) env) env relnames rel_arities in (* and of the real constructors*) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 41a8bdc4c9ec..0d81630d88e6 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1630,9 +1630,8 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls let function_r = ERelevance.relevant in (* TODO relevance *) let env = - EConstr.push_named - (Context.Named.Declaration.LocalAssum - (make_annot function_name function_r, function_type)) + EConstr.push_named ProofVar + (LocalAssum (make_annot function_name function_r, function_type)) env in (* Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *) diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 5920390ea1c1..2a7a7d1038ee 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -118,11 +118,11 @@ let rec add_prods_sign env sigma t = | Prod (na,c1,b) -> let id = id_of_name_using_hdchar env sigma t na.binder_name in let b'= subst1 (mkVar id) b in - add_prods_sign (push_named (LocalAssum ({na with binder_name=id},c1)) env) sigma b' + add_prods_sign (push_named ProofVar (LocalAssum ({na with binder_name=id},c1)) env) sigma b' | LetIn (na,c1,t1,b) -> let id = id_of_name_using_hdchar env sigma t na.binder_name in let b'= subst1 (mkVar id) b in - add_prods_sign (push_named (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b' + add_prods_sign (push_named ProofVar (LocalDef ({na with binder_name=id},c1,t1)) env) sigma b' | _ -> (env,t) (* [dep_option] indicates whether the inversion lemma is dependent or not. @@ -156,8 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let ivars = Termops.global_vars_set env sigma i in let revargs,ownsign = fold_named_context - (fun env d (revargs,hyps) -> - let d = EConstr.of_named_decl d in + (fun env status d (revargs,hyps) -> let id = NamedDecl.get_id d in if Id.Set.mem id ivars then ((mkVar id)::revargs, Context.Named.add d hyps) @@ -170,7 +169,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = (pty,goal) in let npty = nf_all env sigma pty in - let extenv = push_named (LocalAssum (make_annot p ERelevance.relevant,npty)) env in + let extenv = push_named ProofVar (LocalAssum (make_annot p ERelevance.relevant,npty)) env in extenv, goal (* [inversion_scheme sign I] @@ -204,8 +203,7 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context - (fun env d sign -> - let d = EConstr.of_named_decl d in + (fun env status d sign -> if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty diff --git a/plugins/ltac2/tac2core.ml b/plugins/ltac2/tac2core.ml index a31622747735..38ca97720bc7 100644 --- a/plugins/ltac2/tac2core.ml +++ b/plugins/ltac2/tac2core.ml @@ -754,7 +754,7 @@ let () = let sigma, j = Typing.type_judgment env sigma {uj_val=t; uj_type=t_ty} in sigma, EConstr.ESorts.relevance_of_sort j.utj_type in - let nenv = EConstr.push_named (LocalAssum (Context.make_annot id t_rel, t)) env in + let nenv = EConstr.push_named ProofVar (LocalAssum (Context.make_annot id t_rel, t)) env in let (sigma, (evt, s)) = Evarutil.new_type_evar nenv sigma Evd.univ_flexible in let relevance = EConstr.ESorts.relevance_of_sort s in let (sigma, evk) = Evarutil.new_pure_evar (Environ.named_context_val nenv) sigma ~relevance evt in diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml index 823b345fe104..7d4cdc2f20a6 100644 --- a/plugins/micromega/zify.ml +++ b/plugins/micromega/zify.ml @@ -1335,7 +1335,7 @@ let trans_check_prop env evd t = let get_hyp_typ = function | NamedDecl.LocalDef (h, _, ty) | NamedDecl.LocalAssum (h, ty) -> - (h.Context.binder_name, EConstr.of_constr ty) + (h.Context.binder_name, ty) let trans_hyps env evd l = List.fold_left @@ -1449,7 +1449,7 @@ let zify_tac = init_cache (); let evd = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let sign = Environ.named_context env in + let sign = EConstr.named_context env in let concl = Proofview.Goal.concl gl in let evd, concl = trans_check_prop env evd concl in let evd, hyps = trans_hyps env evd sign in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 4d2a659b2702..21224a91bfec 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1203,7 +1203,7 @@ let unsafe_intro env decl ~relevance b = let open Context.Named.Declaration in Refine.refine_with_principal ~typecheck:false begin fun sigma -> let ctx = Environ.named_context_val env in - let nctx = EConstr.push_named_context_val decl ctx in + let nctx = EConstr.push_named_context_val ProofVar decl ctx in let inst = EConstr.identity_subst_val (Environ.named_context_val env) in let ninst = SList.cons (EConstr.mkRel 1) inst in let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in @@ -1212,8 +1212,10 @@ let unsafe_intro env decl ~relevance b = end let set_decl_id id = let open Context in function - | Rel.Declaration.LocalAssum(name,ty) -> Named.Declaration.LocalAssum({name with binder_name=id},ty) - | Rel.Declaration.LocalDef(name,ty,t) -> Named.Declaration.LocalDef({name with binder_name=id},ty,t) + | Rel.Declaration.LocalAssum(name,ty) -> + Named.Declaration.LocalAssum({name with binder_name=id},ty) + | Rel.Declaration.LocalDef(name,ty,t) -> + Named.Declaration.LocalDef({name with binder_name=id},ty,t) let rec decompose_assum env sigma orig_goal = let open Context in diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 20a04f31661a..1a2aaa97c846 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -291,7 +291,7 @@ let intro_clear ids = let env = Proofview.Goal.env gl in let fold (used_ids, clear_ids, ren) id = let new_id = Ssrcommon.mk_anon_id (Id.to_string id) used_ids in - let used_ids = Environ.push_named_context_val (LocalAssum (annotR new_id, mkProp)) used_ids in + let used_ids = Environ.push_named_context_val ProofVar (LocalAssum (annotR new_id, mkProp)) used_ids in (used_ids, new_id :: clear_ids, (id, new_id) :: ren) in let _, clear_ids, ren = List.fold_left fold (Environ.named_context_val env, [], []) ids in @@ -748,9 +748,9 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin if not (EConstr.isVar sigma c) then Ssrcommon.errorstrm Pp.(str "@ can be used with variables only") else match Context.Named.lookup (EConstr.destVar sigma c) hyps with - | Context.Named.Declaration.LocalAssum _ -> + | LocalAssum _ -> Ssrcommon.errorstrm Pp.(str "@ can be used with let-ins only") - | Context.Named.Declaration.LocalDef (name, b, ty) -> + | LocalDef (name, b, ty) -> Unsafe.tclEVARS sigma <*> tclUNIT (true, EConstr.mkLetIn (map_annot Name.mk_name name,b,ty,cl), c, clr) else diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index bd858fc96026..93881ab8f8a3 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -447,7 +447,7 @@ let pr_econstr_pat env sigma c0 = let dummy_prod = mkProd (make_annot Anonymous Sorts.Relevant,mkProp,mkProp) in let na = make_annot (EConstr.destVar sigma ehole_var) Sorts.Relevant in Context.Named.Declaration.(LocalAssum (na, dummy_prod)) in - let env = Environ.push_named dummy_decl env in + let env = Environ.push_named ProofVar dummy_decl env in pr_econstr_env env sigma (wipe_evar c0) (* Turn (new) evars into metas *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 5f7751267b0b..03ecfe8774b0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1818,7 +1818,7 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = debug_ho_unification (fun () -> Pp.(str"abstracted: " ++ prc env_rhs evd rhs')); let () = check_selected_occs env_rhs evd c !occ occs in - let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in + let env_rhs' = push_named ProofVar (NamedDecl.LocalAssum (id,idty)) env_rhs in set_holes env_rhs' evd fixed rhs' subst | [] -> evd, fixed, rhs in diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 11f79dc6968e..367c02df12cc 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -86,7 +86,7 @@ let define_pure_evar_as_product env evd na evk = in let rdom = ESorts.relevance_of_sort u1 in let evd2,rng = - let newenv = push_named (LocalAssum (make_annot id rdom, dom)) evenv in + let newenv = push_named ProofVar (LocalAssum (make_annot id rdom, dom)) evenv in let src = subterm_source evk ~where:Codomain evksrc in let filter = Filter.extend 1 (evar_filter evi) in if Environ.is_impredicative_sort env (ESorts.kind evd1 s) then @@ -139,7 +139,7 @@ let define_pure_evar_as_lambda env evd name evk = map_annot (fun na -> next_name_away_with_default_using_types evenv evd "x" na avoid (Reductionops.whd_evar evd dom)) na in - let newenv = push_named (LocalAssum (id, dom)) evenv in + let newenv = push_named ProofVar (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = subterm_source evk ~where:Body (evar_source evi) in let abstract_arguments = Abstraction.abstract_last (Evd.evar_abstract_arguments evi) in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 2f89f4e578c0..5e07133d88d1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -869,7 +869,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let evd,b = define_evar_from_virtual_equation define_fun env evd src b t_in_sign sign filter inst_in_env in evd, Context.Named.Declaration.LocalDef (id,b,t_in_sign) in - (push_named_context_val d' sign, Filter.extend 1 filter, + (push_named_context_val ProofVar d' sign, Filter.extend 1 filter, SList.cons (mkRel 1) (SList.Skip.map (lift 1) inst_in_env), SList.cons (mkRel 1) (SList.Skip.map (lift 1) inst_in_sign), push_rel d env,evd,Id.Set.add id.binder_name avoid)) diff --git a/pretyping/heads.ml b/pretyping/heads.ml index 39b51b68958c..e5d7397cf866 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -39,7 +39,7 @@ let rec compute_head_const env sigma cst = and compute_head_var env sigma id = match lookup_named id env with | LocalDef (_,c,_) -> kind_of_head env sigma c -| _ -> RigidHead RigidOther +| LocalAssum _ -> RigidHead RigidOther and kind_of_head env sigma t = let rec aux k l t b = match EConstr.kind sigma (Reductionops.clos_whd_flags RedFlags.betaiotazeta env sigma t) with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0a01d343da4c..fa75b12120b5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -2154,6 +2154,7 @@ let get_rigid_evars sigma c = | _ -> EConstr.fold sigma aux vars c in aux Id.Set.empty c +(* XXX should we lose section variable status in the push newdecl cases? *) let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let id = let t = match ty with Some t -> t | None -> get_type_of env sigma c in @@ -2168,13 +2169,12 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = in let likefirst = clause_with_generic_occurrences occs in let mkvarid () = EConstr.mkVar id in - let compute_dependency _ d (remvars,sign,depdecls) = - let d = EConstr.of_named_decl d in + let compute_dependency _ status d (remvars,sign,depdecls) = let hyp = NamedDecl.get_id d in if Id.Set.is_empty remvars then match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> - (remvars,push_named_context_val d sign,depdecls) + (remvars,push_named_context_val status d sign,depdecls) | (AllOccurrences | AtLeastOneOccurrence), InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo env sigma occ test mkvarid d in @@ -2183,17 +2183,17 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = then if check_occs && not (in_every_hyp occs) then raise (PretypeError (env,sigma,NoOccurrenceFound (c,Some hyp))) - else (remvars,push_named_context_val d sign, depdecls) + else (remvars,push_named_context_val status d sign, depdecls) else - (remvars,push_named_context_val newdecl sign, newdecl :: depdecls) + (remvars,push_named_context_val status newdecl sign, newdecl :: depdecls) | occ -> (* There are specific occurrences, hence not like first *) let newdecl = replace_term_occ_decl_modulo env sigma (AtOccs occ) test mkvarid d in - (remvars,push_named_context_val newdecl sign, newdecl :: depdecls) + (remvars,push_named_context_val status newdecl sign, newdecl :: depdecls) else (* Skip declarations if all rigid variables have not been introduced *) let remvars = Id.Set.remove hyp remvars in - (remvars,push_named_context_val d sign,depdecls) + (remvars,push_named_context_val status d sign,depdecls) in let vars = get_rigid_evars sigma c in try diff --git a/printing/printer.ml b/printing/printer.ml index e56dcc7f2a7e..6719789f7bee 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -418,7 +418,7 @@ let pr_erel_decl ?flags env sigma (decl:EConstr.rel_declaration) = (* Prints a signature, all declarations on the same line if possible *) let pr_named_context_of ?flags env sigma = - let make_decl_list env d pps = pr_named_decl ?flags env sigma d :: pps in + let make_decl_list env _status d pps = pr_named_decl ?flags env sigma d :: pps in let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) diff --git a/proofs/logic.ml b/proofs/logic.ml index 25dc273883f5..1f3e0e45271d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -82,28 +82,30 @@ let reorder_context env sigma sign ord = user_err Pp.(str "Order list has duplicates"); let rec step ord expected ctxt_head moved_hyps ctxt_tail = match ord with - | [] -> List.fold_left (fun accu decl -> EConstr.push_named_context_val decl accu) ctxt_head ctxt_tail - | top::ord' when mem_q top moved_hyps -> - let ((d,h),mh) = find_q top moved_hyps in - if occur_vars_in_decl env sigma h d then - user_err - (str "Cannot move declaration " ++ Id.print top ++ spc() ++ - str "before " ++ - pr_sequence Id.print - (Id.Set.elements (Id.Set.inter h - (global_vars_set_of_decl env sigma d))) ++ str "."); - step ord' expected ctxt_head mh (d::ctxt_tail) - | _ -> - (match EConstr.match_named_context_val ctxt_head with - | None -> error_no_such_hypothesis env sigma (List.hd ord) - | Some (d, ctxt) -> - let x = NamedDecl.get_id d in - if Id.Set.mem x expected then - step ord (Id.Set.remove x expected) - ctxt (push_item x d moved_hyps) ctxt_tail - else - step ord expected - ctxt (push_val x moved_hyps) (d::ctxt_tail)) in + | [] -> + List.fold_left (fun accu (status,decl) -> EConstr.push_named_context_val status decl accu) + ctxt_head ctxt_tail + | top::ord' when mem_q top moved_hyps -> + let (((status,d),h),mh) = find_q top moved_hyps in + if occur_vars_in_decl env sigma h d then + user_err + (str "Cannot move declaration " ++ Id.print top ++ spc() ++ + str "before " ++ + pr_sequence Id.print + (Id.Set.elements (Id.Set.inter h (global_vars_set_of_decl env sigma d))) ++ + str "."); + step ord' expected ctxt_head mh ((status,d)::ctxt_tail) + | _ -> + (match EConstr.match_named_context_val ctxt_head with + | None -> error_no_such_hypothesis env sigma (List.hd ord) + | Some (status, d, ctxt) -> + let x = NamedDecl.get_id d in + if Id.Set.mem x expected then + step ord (Id.Set.remove x expected) + ctxt (push_item x (status, d) moved_hyps) ctxt_tail + else + step ord expected + ctxt (push_val x moved_hyps) ((status,d)::ctxt_tail)) in step ord ords sign mt_q [] let reorder_val_context env sigma sign ord = @@ -156,10 +158,10 @@ let split_sign env sigma hfrom l = let () = if not (mem_id_context hfrom l) then error_no_such_hypothesis env sigma hfrom in let rec splitrec left sign = match EConstr.match_named_context_val sign with | None -> assert false - | Some (d, right) -> + | Some (status, d, right) -> let hyp = NamedDecl.get_id d in - if Id.equal hyp hfrom then (left, right, d) - else splitrec (d :: left) right + if Id.equal hyp hfrom then (left, right, (status, d)) + else splitrec ((status, d) :: left) right in splitrec [] l @@ -177,21 +179,26 @@ let () = CErrors.register_handler (function let move_hyp env sigma toleft (left,declfrom,right) hto = let open EConstr in - let push prefix sign = List.fold_right push_named_context_val prefix sign in - let push_rev prefix sign = List.fold_left (fun accu d -> push_named_context_val d accu) sign prefix in + let idfrom = NamedDecl.get_id (snd declfrom) in + let push prefix sign = + List.fold_right (fun (status,d) sign -> push_named_context_val status d sign) prefix sign + in + let push_rev prefix sign = + List.fold_left (fun accu (status,d) -> push_named_context_val status d accu) sign prefix + in let rec moverec_toleft ans first middle midvars = function | [] -> push middle @@ push first ans - | d :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> + | (_, d) :: _ as right when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> push_rev right @@ push middle @@ push first ans - | d :: right -> + | (status, d) :: right -> let hyp = NamedDecl.get_id d in let (first', middle', midvars') = if occur_vars_in_decl env sigma midvars d then if not (move_location_eq hto (MoveAfter hyp)) then - (first, d :: middle, Id.Set.add hyp midvars) - else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp}) + (first, (status, d) :: middle, Id.Set.add hyp midvars) + else raise (CannotMoveHyp {from = idfrom; hto; hyp}) else - (d::first, middle, midvars) + ((status,d)::first, middle, midvars) in if move_location_eq hto (MoveAfter hyp) then push_rev right @@ push middle' @@ push first' ans @@ -200,19 +207,19 @@ let move_hyp env sigma toleft (left,declfrom,right) hto = in let rec moverec_toright first middle depvars right = match EConstr.match_named_context_val right with | None -> push_rev first @@ push_rev middle right - | Some (d, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> + | Some (status, d, _) when move_location_eq hto (MoveBefore (NamedDecl.get_id d)) -> push_rev first @@ push_rev middle @@ right - | Some (d, right) -> + | Some (status, d, right) -> let hyp = NamedDecl.get_id d in let (first', middle', depvars') = if Id.Set.mem hyp depvars then if not (move_location_eq hto (MoveAfter hyp)) then let vars = global_vars_set_of_decl env sigma d in let depvars = Id.Set.union vars depvars in - (first, d::middle, depvars) - else raise (CannotMoveHyp {from = NamedDecl.get_id declfrom; hto; hyp}) + (first, (status, d)::middle, depvars) + else raise (CannotMoveHyp {from = idfrom; hto; hyp}) else - (d::first, middle, depvars) + ((status,d)::first, middle, depvars) in if move_location_eq hto (MoveAfter hyp) then push_rev first' @@ push_rev middle' @@ right @@ -220,10 +227,9 @@ let move_hyp env sigma toleft (left,declfrom,right) hto = moverec_toright first' middle' depvars' right in if toleft then - let id = NamedDecl.get_id declfrom in - moverec_toleft right [] [declfrom] (Id.Set.singleton id) left + moverec_toleft right [] [declfrom] (Id.Set.singleton idfrom) left else - let depvars = global_vars_set_of_decl env sigma declfrom in + let depvars = global_vars_set_of_decl env sigma (snd declfrom) in let right = moverec_toright [] [declfrom] depvars right in push_rev left @@ right @@ -258,6 +264,6 @@ let convert_hyp ~check ~reorder env sigma d = if check && not (Option.equal (is_conv env sigma) b c) then user_err (str "Incorrect change of the body of "++ Id.print id ++ str "."); - let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in + let sign' = apply_to_hyp sign id (fun _ status _ _ -> status, EConstr.Unsafe.to_named_decl d) in if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d) else sign' diff --git a/proofs/logic.mli b/proofs/logic.mli index 1983c8b6f49f..32a3f92c8b34 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -61,5 +61,5 @@ val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move Environ.named_context_val -> Environ.named_context_val val insert_decl_in_named_context : Environ.env -> Evd.evar_map -> - EConstr.named_declaration -> Id.t move_location -> + Environ.var_status * EConstr.named_declaration -> Id.t move_location -> Environ.named_context_val -> Environ.named_context_val diff --git a/proofs/refine.ml b/proofs/refine.ml index 1068d0d94dbd..d7f378482404 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -17,30 +17,38 @@ module NamedDecl = Context.Named.Declaration let extract_prefix env info = let ctx1 = List.rev (EConstr.named_context env) in let ctx2 = List.rev (Evd.evar_context info) in - let rec share l1 l2 accu = match l1, l2 with + let rec share l1 l2 = match l1, l2 with | d1 :: l1, d2 :: l2 -> - if d1 == d2 then share l1 l2 (d1 :: accu) - else (accu, d2 :: l2) - | _ -> (accu, l2) + if d1 == d2 then share l1 l2 + else 1 + List.length l2 + | _ -> List.length l2 in - share ctx1 ctx2 [] + share ctx1 ctx2 + +let rec recheck_hyps n env sigma sign = + if n = 0 then sigma + else match EConstr.match_named_context_val sign with + | None -> assert false + | Some (_, decl, sign') -> + let sigma = recheck_hyps (n-1) env sigma sign' in + let env = Environ.reset_with_named_context sign' env in + let t = NamedDecl.get_type decl in + let sigma, _ = Typing.sort_of env sigma t in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,body,_) -> Typing.check env sigma body t + in + sigma let typecheck_evar ev env sigma = let info = Evd.find_undefined sigma ev in + (* optim: avoid checking unchanged hyps *) + let changed = extract_prefix env info in (* Typecheck the hypotheses. *) - let type_hyp (sigma, env) decl = - let t = NamedDecl.get_type decl in - let sigma, _ = Typing.sort_of env sigma t in - let sigma = match decl with - | LocalAssum _ -> sigma - | LocalDef (_,body,_) -> Typing.check env sigma body t - in - (sigma, EConstr.push_named decl env) - in - let (common, changed) = extract_prefix env info in - let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in - let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in + let sign = Evd.evar_hyps info in + let sigma = recheck_hyps changed env sigma sign in (* Typecheck the conclusion *) + let env = Environ.reset_with_named_context sign env in let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in sigma diff --git a/proofs/subproof.ml b/proofs/subproof.ml index b4af1fa69769..ca1f9b1b24b7 100644 --- a/proofs/subproof.ml +++ b/proofs/subproof.ml @@ -139,7 +139,7 @@ let build_constant_by_tactic ~name ~sigma ~env ~sign ~poly typ tac = let build_by_tactic env ~uctx ~poly ~typ tac = let name = Id.of_string "temporary_proof" in - let sign = Environ.(val_of_named_context (named_context env)) in + let sign = Environ.named_context_val env in let sigma = Evd.from_ustate uctx in (* status doesn't matter: any given up evars can't be in the body/typ (we would get OpenProof exception) and we drop the evar part of the evar map *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 95f62ab1e9c0..a1da48783ef7 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -15,7 +15,6 @@ open Reductionops open Typing open Tacred open Logic -open Context.Named.Declaration module NamedDecl = Context.Named.Declaration @@ -63,10 +62,8 @@ let pf_get_hyp_typ id gl = let pf_hyps_types gl = let env = Proofview.Goal.env gl in - let sign = Environ.named_context env in - List.map (function LocalAssum (id,x) - | LocalDef (id,_,x) -> id.Context.binder_name, EConstr.of_constr x) - sign + let sign = EConstr.named_context env in + List.map (fun d -> NamedDecl.get_id d, NamedDecl.get_type d) sign let pf_last_hyp gl = let hyps = Proofview.Goal.hyps gl in diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 7faf77ba3973..417c60dd35ad 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -9,7 +9,6 @@ (************************************************************************) open Util -open Termops open EConstr module NamedDecl = Context.Named.Declaration @@ -18,23 +17,6 @@ module NamedDecl = Context.Named.Declaration the current goal, abstracted with respect to the local signature, is solved by tac *) -(** d1 is the section variable in the global context, d2 in the goal context *) -let interpretable_as_section_decl env sigma d1 d2 = - let open Context.Named.Declaration in - let e_eq_constr_univs sigma c1 c2 = match eq_constr_universes env sigma c1 c2 with - | None -> false - | Some cstr -> - try - let _sigma = Evd.add_constraints sigma cstr in - true - with UGraph.UniverseInconsistency _ | UState.UniversesDiffer -> false - in - match d2, d1 with - | LocalDef _, LocalAssum _ -> false - | LocalDef (_,b1,t1), LocalDef (_,b2,t2) -> - e_eq_constr_univs sigma b1 b2 && e_eq_constr_univs sigma t1 t2 - | LocalAssum (_,t1), d2 -> e_eq_constr_univs sigma t1 (NamedDecl.get_type d2) - let name_op_to_name ~name_op ~name suffix = match name_op with | Some s -> s @@ -56,11 +38,9 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let sign,secsign = List.fold_right (fun d (s1,s2) -> - let id = NamedDecl.get_id d in - if mem_named_context_val id section_sign && - interpretable_as_section_decl env sigma (lookup_named_val id section_sign) d - then (s1,push_named_context_val d s2) - else (Context.Named.add d s1,s2)) + match Environ.var_status (NamedDecl.get_id d) env with + | SecVar -> (s1,push_named_context_val SecVar d s2) + | ProofVar -> (Context.Named.add d s1,s2)) goal_sign (Context.Named.empty, Environ.empty_named_context_val) in let bad id = match lookup_named_val id section_sign with diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b4dcceffbf02..8a46776ac73d 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -442,10 +442,10 @@ let make_resolve_hyp env sigma st only_classes decl db = push_resolves env sigma id db else db -let make_hints env sigma (modes,st) only_classes sign = +let make_hints env sigma (modes,st) only_classes = let db = Hint_db.add_modes modes @@ Hint_db.empty st true in - List.fold_right - (fun hyp hints -> + EConstr.fold_named_context + (fun _ status hyp hints -> let consider = not only_classes || try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in @@ -456,7 +456,7 @@ let make_hints env sigma (modes,st) only_classes sign = if consider then make_resolve_hyp env sigma st only_classes hyp hints else hints) - sign db + env ~init:db module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) @@ -498,7 +498,7 @@ module Search = struct cached_modes == modes then cached_hints else - let hints = make_hints env sigma mst only_classes sign in + let hints = make_hints env sigma mst only_classes in autogoal_cache := (cwd, only_classes, sign, modes, hints, qvars); hints let make_autogoal env sigma mst only_classes dep cut best_effort i = diff --git a/tactics/equality.ml b/tactics/equality.ml index 77431b5a7e45..59e7a64547ae 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1186,7 +1186,7 @@ let discr_positions env sigma { eq_data = (_, _ , s, (t, _, _)) as eq_data; eq_t let false_ty = Retyping.get_type_of env sigma false_0 in let false_kind = Retyping.get_sort_of env sigma false_0 in let e = next_ident_away eq_baseid (vars_of_env env) in - let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e ERelevance.relevant,t)) env in + let e_env = push_named ProofVar (LocalAssum (make_annot e ERelevance.relevant,t)) env in let discriminator = try @@ -1415,7 +1415,7 @@ let simplify_args env sigma t = let inject_at_positions env sigma l2r eq posns tac = let { eq_data = (eq, congr, s, (t,t1,t2)); eq_term = v; eq_evar = evs } = eq in let e = next_ident_away eq_baseid (vars_of_env env) in - let e_env = push_named (LocalAssum (make_annot e ERelevance.relevant,t)) env in + let e_env = push_named ProofVar (LocalAssum (make_annot e ERelevance.relevant,t)) env in let evdref = ref sigma in let filter (cpath, t1', t2') = try diff --git a/tactics/fixTactics.ml b/tactics/fixTactics.ml index 4b44217c33eb..a2179cf62420 100644 --- a/tactics/fixTactics.ml +++ b/tactics/fixTactics.ml @@ -55,7 +55,7 @@ let mutual_fix f n others = Proofview.Goal.enter begin fun gl -> let () = check_mutind env sigma n ar in if mem_named_context_val f sign then TacticErrors.intro_already_declared f; - mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth + mk_sign (push_named_context_val ProofVar (LocalAssum (make_annot f r, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine ~typecheck:false begin fun sigma -> @@ -98,7 +98,7 @@ let mutual_cofix f others = Proofview.Goal.enter begin fun gl -> let open Context.Named.Declaration in if mem_named_context_val f sign then TacticErrors.already_used f; - mk_sign (push_named_context_val (LocalAssum (make_annot f r, ar)) sign) oth + mk_sign (push_named_context_val ProofVar (LocalAssum (make_annot f r, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in Refine.refine ~typecheck:false begin fun sigma -> diff --git a/tactics/induction.ml b/tactics/induction.ml index 553fcdfdbfeb..02c5b6f75c67 100644 --- a/tactics/induction.ml +++ b/tactics/induction.ml @@ -216,10 +216,10 @@ let insert_before decls lasthyp env = | None -> push_named_context decls env | Some id -> Environ.fold_named_context - (fun _ d env -> + (fun _ status d env -> let d = EConstr.of_named_decl d in let env = if Id.equal id (NamedDecl.get_id d) then push_named_context decls env else env in - push_named d env) + push_named status d env) ~init:(reset_context env) env let mk_eq_name env id {CAst.loc;v=ido} = @@ -237,8 +237,8 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty = let open Context.Named.Declaration in let t = match ty with Some t -> t | _ -> typ_of env sigma c in let r = Retyping.relevance_of_type env sigma t in - let decl = if dep then LocalDef (make_annot id r,c,t) - else LocalAssum (make_annot id r,t) + let decl = if dep then LocalDef (make_annot id r, c, t) + else LocalAssum (make_annot id r, t) in match with_eq with | Some (lr,heq) -> @@ -251,13 +251,13 @@ let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty = let sigma, eq = Typing.checked_applist env sigma eq [t] in let eq = applist (eq,args) in let refl = applist (refl, [t;mkVar id]) in - let newenv = insert_before [LocalAssum (make_annot heq ERelevance.relevant,eq); decl] lastlhyp env in + let newenv = insert_before [ProofVar, LocalAssum (make_annot heq ERelevance.relevant,eq); ProofVar, decl] lastlhyp env in let (sigma, x) = new_evar newenv sigma ccl in (sigma, mkNamedLetIn sigma (make_annot id r) c t (mkNamedLetIn sigma (make_annot heq ERelevance.relevant) refl eq x), Some (fst @@ destEvar sigma x)) | None -> - let newenv = insert_before [decl] lastlhyp env in + let newenv = insert_before [ProofVar, decl] lastlhyp env in let (sigma, x) = new_evar newenv sigma ccl in (sigma, mkNamedLetIn sigma (make_annot id r) c t x, Some (fst @@ destEvar sigma x)) @@ -589,8 +589,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = let lstatus = ref [] in let before = ref true in let maindep = ref false in - let seek_deps env decl rhyp = - let decl = EConstr.of_named_decl decl in + let seek_deps env _ decl rhyp = let hyp = NamedDecl.get_id decl in if (match hyp0_opt with Some hyp0 -> Id.equal hyp hyp0 | _ -> false) then begin diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml index c2011de9df77..24276be57f82 100644 --- a/tactics/rewrite.ml +++ b/tactics/rewrite.ml @@ -838,7 +838,7 @@ let resolve_morphism env m args args' (b,cstr) evars = let _, dosub = app_poly_sort b env evars dosub [||] in let _, appsub = app_poly_nocheck env evars appsub [||] in let dosub_id = Id.of_string "do_subrelation" in - let env' = EConstr.push_named (LocalDef (make_annot dosub_id ERelevance.relevant, dosub, appsub)) env in + let env' = EConstr.push_named ProofVar (LocalDef (make_annot dosub_id ERelevance.relevant, dosub, appsub)) env in let evars, morph = new_cstr_evar evars env' app in (* Replace the free [dosub_id] in the evar by the global reference *) let morph = Vars.replace_vars (fst evars) [dosub_id , dosub] morph in @@ -1745,8 +1745,8 @@ let cl_rewrite_clause_newtac ?origsigma ~progress abs strat clause = | None -> env | Some id -> (* Only consider variables not depending on [id] *) - let ctx = named_context env in - let filter decl = not (occur_var_in_decl env sigma id decl) in + let ctx = named_context_of_val_with_status @@ named_context_val env in + let filter (_, decl) = not (occur_var_in_decl env sigma id decl) in let nctx = List.filter filter ctx in Environ.reset_with_named_context (val_of_named_context nctx) env in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 907bceb5051b..61db30f713cf 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -81,8 +81,8 @@ let () = let unsafe_intro env decl ~relevance b = Refine.refine_with_principal ~typecheck:false begin fun sigma -> let ctx = named_context_val env in - let nctx = push_named_context_val decl ctx in - let inst = EConstr.identity_subst_val (named_context_val env) in + let nctx = push_named_context_val ProofVar decl ctx in + let inst = EConstr.identity_subst_val ctx in let ninst = SList.cons (mkRel 1) inst in let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in let (sigma, ev) = new_pure_evar nctx sigma ~relevance nb in @@ -259,13 +259,17 @@ let rename_hyp repl = let make_subst (src, dst) = (src, mkVar dst) in let subst = List.map make_subst repl in let subst c = Vars.replace_vars sigma subst c in - let replace id = try List.assoc_f Id.equal id repl with Not_found -> id in - let map decl = decl |> NamedDecl.map_id replace |> NamedDecl.map_constr subst in - let ohyps = named_context_of_val sign in + let map (status, decl) = + let decl = NamedDecl.map_constr subst decl in + match List.assoc_f_opt Id.equal (NamedDecl.get_id decl) repl with + | None -> status, decl + | Some id -> ProofVar, NamedDecl.set_id id decl + in + let ohyps = EConstr.named_context_of_val_with_status @@ Environ.named_context_val env in let nhyps = List.map map ohyps in let nconcl = subst concl in let nctx = val_of_named_context nhyps in - let fold odecl ndecl accu = + let fold (_,odecl) (_,ndecl) accu = if Id.equal (NamedDecl.get_id odecl) (NamedDecl.get_id ndecl) then SList.default accu else @@ -379,12 +383,12 @@ let internal_cut ?(check=true) replace id t = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in - let sign' = insert_decl_in_named_context env sigma (LocalAssum (make_annot id r,t)) nexthyp sign' in + let sign' = insert_decl_in_named_context env sigma (ProofVar,LocalAssum (make_annot id r,t)) nexthyp sign' in Environ.reset_with_named_context sign' env,t,concl,sigma else (if check && mem_named_context_val id sign then TacticErrors.intro_already_declared id; - push_named (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in + push_named ProofVar (LocalAssum (make_annot id r,t)) env,t,concl,sigma) in let nf_t = nf_betaiota env sigma t in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -443,6 +447,7 @@ let[@ocaml.inline] (let*) m f = match m with | NoChange -> NoChange | Changed v -> f v +(* should secvar status change when Changed? *) let e_pf_change_decl (redfun : bool -> Tacred.change_function) where env sigma decl = let open Context.Named.Declaration in match decl with @@ -531,7 +536,7 @@ let e_change_in_hyps ~check ~reorder f args = match args with in let reds = List.fold_left fold Id.Map.empty args in let evdref = ref sigma in - let map d = + let map status d = let id = NamedDecl.get_id d in match Id.Map.find id reds with | reds -> @@ -542,8 +547,8 @@ let e_change_in_hyps ~check ~reorder f args = match args with in let (sigma, d) = List.fold_right fold reds (sigma, d) in let () = evdref := sigma in - EConstr.Unsafe.to_named_decl d - | exception Not_found -> d + status, EConstr.Unsafe.to_named_decl d + | exception Not_found -> status, d in let sign = Environ.map_named_val map (Environ.named_context_val env) in let env = reset_with_named_context sign env in @@ -947,7 +952,7 @@ let intro_forthcoming_last_then_gen avoid dep_flag bound n tac = if List.is_empty ids then tac [] else Refine.refine_with_principal ~typecheck:false begin fun sigma -> let ctx = named_context_val env in - let nctx = List.fold_right push_named_context_val ndecls ctx in + let nctx = List.fold_right (fun d ctx -> push_named_context_val ProofVar d ctx) ndecls ctx in let inst = SList.defaultn (List.length @@ Environ.named_context env) SList.empty in let rels = List.init (List.length decls) (fun i -> mkRel (i + 1)) in let ninst = List.fold_right (fun c accu -> SList.cons c accu) rels inst in @@ -1916,7 +1921,7 @@ let clear_body idl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in let sigma = Proofview.Goal.sigma gl in - let ctx = named_context env in + let ctx = named_context_of_val_with_status (named_context_val env) in let ids = Id.Set.of_list idl in let () = match Id.Set.find_first_opt (fun v -> not (mem_named v env)) ids with @@ -1932,7 +1937,7 @@ let clear_body idl = else match ctx with | [] -> assert false - | decl :: ctx -> + | (status, decl) :: ctx -> let decl, ids, found = match decl with | LocalAssum (id,t) -> @@ -1950,9 +1955,9 @@ let clear_body idl = if Id.Set.exists (fun id -> occur_var_in_decl env sigma id decl) ids then let sigma = check_decl env sigma idl ids decl in (* can sigma really change? *) let ids = Id.Set.add (get_id decl) ids in - push_named decl env, sigma, Id.Set.add (get_id decl) ids + push_named status decl env, sigma, Id.Set.add (get_id decl) ids else - push_named decl env, sigma, if found then Id.Set.add (get_id decl) ids else ids + push_named status decl env, sigma, if found then Id.Set.add (get_id decl) ids else ids in try let env, sigma, ids = fold ids ctx in @@ -2534,7 +2539,7 @@ let pose_tac na c = Proofview.Unsafe.tclEVARS sigma <*> Refine.refine ~typecheck:false begin fun sigma -> let id = make_annot id rel in - let nhyps = EConstr.push_named_context_val (NamedDecl.LocalDef (id, c, t)) hyps in + let nhyps = EConstr.push_named_context_val ProofVar (NamedDecl.LocalDef (id, c, t)) hyps in let (sigma, ev) = Evarutil.new_pure_evar nhyps sigma ~relevance concl in let inst = EConstr.identity_subst_val hyps in let body = mkEvar (ev, SList.cons (mkRel 1) inst) in diff --git a/test-suite/bugs/bug_6773.v b/test-suite/bugs/bug_6773.v new file mode 100644 index 000000000000..4a8f0dc8095b --- /dev/null +++ b/test-suite/bugs/bug_6773.v @@ -0,0 +1,14 @@ +Section BuggySection. + + Variable B: nat. + + Axiom F: False. (* To replace admits, allowing QED in bug*) + + Lemma BUG (i: nat) : False. + Proof. + induction i in B. + assert (B = B) by abstract reflexivity. + all: now destruct F. (* No more subgoals. *) + Qed. (* fails *) + +End BuggySection. diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 8af3fa4a8822..dccd0d827cda 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -452,7 +452,7 @@ let interp_mutual_definition env ~program_mode ~poly ~function_mode rec_order fi List.fold_left4 (fun (sigma, rec_sign) id r t (_,extradecl) -> let sigma, r, t = if program_mode && List.is_empty extradecl then encapsulate env sigma r t else sigma, r, t in - sigma, LocalAssum (Context.make_annot id r, t) :: rec_sign) + sigma, (Environ.ProofVar, LocalAssum (Context.make_annot id r, t)) :: rec_sign) (sigma, []) fixnames fixrs fixtypes fixextras in let fixrecimps = List.map3 (fun ctximps wfimps cclimps -> ctximps @ wfimps @ cclimps) fixctximps fixwfimps fixcclimps in @@ -470,7 +470,7 @@ let interp_mutual_definition env ~program_mode ~poly ~function_mode rec_order fi (fun sigma fixctximpenv (after,extradecl) ctx body ccl -> let impls = Id.Map.fold Id.Map.add fixctximpenv impls in let env', ctx = - if after then env, List.map NamedDecl.to_rel_decl rec_sign @ ctx + if after then env, List.map (fun (_,d) -> NamedDecl.to_rel_decl d) rec_sign @ ctx else push_named_context rec_sign env, extradecl@ctx in interp_fix_body ~program_mode env' ctx sigma impls body (Vars.lift (Context.Rel.length extradecl) ccl)) sigma fixctximpenvs fixextras fixctxs fixl fixccls) diff --git a/vernac/declare.ml b/vernac/declare.ml index 8bc033f82fa2..a7fa69557df4 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -1832,7 +1832,7 @@ let initialize_named_context_for_proof () = (fun d signv -> let id = NamedDecl.get_id d in let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in - Environ.push_named_context_val d signv) sign Environ.empty_named_context_val + Environ.push_named_context_val SecVar d signv) sign Environ.empty_named_context_val let start_proof_core ~name ~pinfo ?using sigma goals = (* In ?sign, we remove the bodies of variables in the named context @@ -1919,7 +1919,7 @@ let start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma = let sign = List.fold_left2 (fun sign CInfo.{name;typ} r -> let decl = Context.Named.Declaration.LocalAssum (Context.make_annot name r, typ) in - EConstr.push_named_context_val decl sign) (initialize_named_context_for_proof ()) cinfo' fixrs in + EConstr.push_named_context_val ProofVar decl sign) (initialize_named_context_for_proof ()) cinfo' fixrs in let using = Option.map (interp_proof_using_cinfo env sigma cinfo') using in let goals = List.map (function CInfo.{typ} -> (Some sign, typ)) thms in let lemma = start_proof_core ~name ~pinfo ?using sigma goals in @@ -1929,7 +1929,9 @@ let start_mutual_definitions ~info ~cinfo ~bodies ~possible_guard ?using sigma = (* Temporary declaration of notations for the time of the proofs *) let ntn_env = (* We simulate the goal context in which the fixpoint bodies have to be proved (exact relevance does not matter) *) - let make_decl CInfo.{name; typ} = Context.Named.Declaration.LocalAssum (Context.annotR name, typ) in + let make_decl CInfo.{name; typ} = + Environ.ProofVar, Context.Named.Declaration.LocalAssum (Context.annotR name, typ) + in Environ.push_named_context (List.map make_decl cinfo) (Global.env()) in List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) ntn_env) info.ntns in lemma @@ -1955,7 +1957,7 @@ let start_mutual_definitions_refine ~info ~cinfo ~bodies ~possible_guard ?using let sign = List.fold_left2 (fun sign CInfo.{name;typ} r -> let decl = Context.Named.Declaration.LocalAssum (Context.make_annot name r, typ) in - EConstr.push_named_context_val decl sign) (initialize_named_context_for_proof ()) cinfo fixrs in + EConstr.push_named_context_val ProofVar decl sign) (initialize_named_context_for_proof ()) cinfo fixrs in let using = Option.map (interp_proof_using_cinfo env sigma cinfo) using in let goals = List.map (function CInfo.{typ} -> (Some sign, typ)) thms in let lemma = start_proof_core ~name ~pinfo ?using sigma goals in @@ -1970,7 +1972,9 @@ let start_mutual_definitions_refine ~info ~cinfo ~bodies ~possible_guard ?using (* Temporary declaration of notations for the time of the proofs *) let ntn_env = (* We simulate the goal context in which the fixpoint bodies have to be proved (exact relevance does not matter) *) - let make_decl CInfo.{name; typ} = Context.Named.Declaration.LocalAssum (Context.annotR name, EConstr.Unsafe.to_constr typ) in + let make_decl CInfo.{name; typ} = + Environ.ProofVar, Context.Named.Declaration.LocalAssum (Context.annotR name, EConstr.Unsafe.to_constr typ) + in Environ.push_named_context (List.map make_decl cinfo) (Global.env()) in List.iter (Metasyntax.add_notation_interpretation ~local:(info.scope=Locality.Discharge) ntn_env) info.ntns in lemma @@ -1986,7 +1990,7 @@ let set_used_variables ps ~using = let ctx_set = List.fold_right Id.Set.add (List.map NamedDecl.get_id ctx) Id.Set.empty in let vars_of = Environ.global_vars_set in - let aux env entry (ctx, all_safe as orig) = + let aux env _status entry (ctx, all_safe as orig) = match entry with | LocalAssum ({Context.binder_name=x},_) -> if Id.Set.mem x all_safe then orig diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml index 3afbdbf0c322..d2989166ab54 100644 --- a/vernac/retrieveObl.ml +++ b/vernac/retrieveObl.ml @@ -237,6 +237,8 @@ let retrieve_obligations env name evm fs ?deps ?status t ty = List.fold_right (fun (id, (n, nstr), ev) evs -> let hyps = Evd.evar_filtered_context ev in + (* XXX ignore vars based on secvar status + names of recursive functions + instead of length of global context + number of recursive functions *) let hyps = trunc_named_context nc_len hyps in let evtyp, deps, transp = etype_of_evar evm evs hyps (Evd.evar_concl ev) in let evtyp, hyps, chop = From 45e9c605df868e94d8161d156decdefe8a84be90 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 30 Apr 2026 14:52:54 +0200 Subject: [PATCH 02/17] check_hyps_inclusion use variable status instead of conversion This lets us detect if a variable is some unrelated variable which got renamed to the name of a previously cleared section variable. It's also cheaper than conversion but that's not really the point of this patch. Fix #11487 --- kernel/typeops.ml | 39 +++++++++-------------------------- kernel/typeops.mli | 3 +-- pretyping/inductiveops.ml | 4 ++-- pretyping/reductionops.ml | 5 ----- pretyping/reductionops.mli | 3 --- pretyping/retyping.ml | 2 +- pretyping/typing.ml | 11 +++++----- test-suite/bugs/bug_11487.v | 16 ++++++++++++++ test-suite/bugs/bug_20847_1.v | 18 ++++++++++++++++ 9 files changed, 54 insertions(+), 47 deletions(-) create mode 100644 test-suite/bugs/bug_11487.v create mode 100644 test-suite/bugs/bug_20847_1.v diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 6aebeaeae274..7657a7741223 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -170,35 +170,16 @@ let type_of_variable env id = (* Management of context of variables. *) (* Checks if a context of variables can be instantiated by the - variables of the current env. - Order does not have to be checked assuming that all names are distinct *) -(* TODO use var status instead *) -let check_hyps_inclusion env ?evars c sign = - let conv env a b = conv env ?evars a b in - Context.Named.fold_outside - (fun d1 () -> - let open Context.Named.Declaration in - let id = NamedDecl.get_id d1 in - try - let d2 = lookup_named id env in - let () = match conv env (get_type d2) (get_type d1) with - | Result.Ok () -> () - | Result.Error () -> raise NotConvertible - in - (match d2,d1 with - | LocalAssum _, LocalAssum _ -> () - | LocalAssum _, LocalDef _ -> - (* This is wrong, because we don't know if the body is - needed or not for typechecking: *) () - | LocalDef _, LocalAssum _ -> raise NotConvertible - | LocalDef (_,b2,_), LocalDef (_,b1,_) -> - match conv env b2 b1 with - | Result.Ok () -> () - | Result.Error () -> raise NotConvertible); - with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id c) - sign - ~init:() + variables of the current env. *) +let check_hyps_inclusion env c sign = + sign |> List.iter @@ fun d -> + let id = NamedDecl.get_id d in + let ok = + match var_status ~check:false id env with + | SecVar -> true + | ProofVar -> false + in + if not ok then error_reference_variables env id c (* Instantiation of terms on real arguments. *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index d9a47916cc16..c0d94ec8d555 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -72,8 +72,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * UVars.AbstractContex (** {6 Miscellaneous. } *) (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ?evars:CClosure.evar_handler -> - GlobRef.t -> Constr.named_context -> unit +val check_hyps_inclusion : env -> GlobRef.t -> Constr.named_context -> unit (** Types for primitives *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 1d8452d3b9d6..0fed7ee86bd1 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -31,7 +31,7 @@ let type_of_inductive env (ind,u) = let e_type_of_inductive env sigma (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Reductionops.check_hyps_inclusion env sigma (GlobRef.IndRef ind) mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t = Inductive.type_of_inductive (specif, EConstr.Unsafe.to_instance u) in EConstr.of_constr (Arguments_renaming.rename_type env t (IndRef ind)) @@ -47,7 +47,7 @@ let type_of_constructor env (cstr,u) = let e_type_of_constructor env sigma (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Reductionops.check_hyps_inclusion env sigma (GlobRef.ConstructRef cstr) mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps; let t = Inductive.type_of_constructor (cstr,EConstr.Unsafe.to_instance u) specif in EConstr.of_constr (Arguments_renaming.rename_type env t (ConstructRef cstr)) diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9195b1a1f216..e99e4ea1ee4d 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1414,11 +1414,6 @@ let native_infer_conv ?(pb=Conversion.CUMUL) env sigma t1 t2 = infer_conv_gen { genconv = fun pb ~l2r sigma ts -> native_conv_generic pb sigma } ~catch_incon:true ~pb env sigma t1 t2 -let check_hyps_inclusion env sigma x hyps = - let env = Environ.set_universes (Evd.universes sigma) env in - let evars = Evd.evar_handler sigma in - Typeops.check_hyps_inclusion env ~evars x hyps - (********************************************************************) (* Special-Purpose Reduction *) (********************************************************************) diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index f003559812f0..2e3df384cd9c 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -283,9 +283,6 @@ val infer_conv_gen : genconv -> ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> evar_map option -val check_hyps_inclusion : env -> evar_map -> GlobRef.t -> Constr.named_context -> unit -(** [Typeops.check_hyps_inclusion] but handles evars in the environment. *) - (** {6 Heuristic for Conversion with Evar } *) type state = constr * Stack.t diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 35cef4bd6ca0..8d27c6126dc1 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -136,7 +136,7 @@ let betazetaevar_applist sigma n c l = let type_of_constant env sigma (c,u) = let cb = lookup_constant env sigma c in - let () = check_hyps_inclusion env sigma (GlobRef.ConstRef c) cb.const_hyps in + let () = Typeops.check_hyps_inclusion env (GlobRef.ConstRef c) cb.const_hyps in let ty = CVars.subst_instance_constr (EConstr.Unsafe.to_instance u) cb.const_type in EConstr.of_constr (rename_type env ty (GlobRef.ConstRef c)) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 78fbf193b775..c540c10f6da1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -135,9 +135,10 @@ let judge_of_applied ~check env sigma funj argjv = let typ = hnf_prod_appvect env sigma (j_type funj) (Array.map j_val argjv) in sigma, { uj_val = (mkApp (j_val funj, Array.map j_val argjv)); uj_type = typ } +(* XXX check_hyps_inclusion should now be cheap enough to always do *) let judge_of_applied_inductive_knowing_parameters ~check env sigma (ind, u) argjv = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in + let () = if check then Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in let sigma, paramstyp = fresh_template_context env sigma ind specif argjv in let u0 = EInstance.kind sigma u in let ty, csts = Inductive.type_of_inductive_knowing_parameters (specif, u0) paramstyp in @@ -147,7 +148,7 @@ let judge_of_applied_inductive_knowing_parameters ~check env sigma (ind, u) argj let judge_of_applied_constructor_knowing_parameters ~check env sigma ((ind, _ as cstr), u) argjv = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = if check then Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in + let () = if check then Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in let sigma, paramstyp = fresh_template_context env sigma ind specif argjv in let u0 = EInstance.kind sigma u in let ty, csts = Inductive.type_of_constructor_knowing_parameters (cstr, u0) specif paramstyp in @@ -413,7 +414,7 @@ let judge_of_letin env sigma name defj typj j = let type_of_constant env sigma (c,u) = let open Declarations in let cb = EConstr.lookup_constant env sigma c in - let () = Reductionops.check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in + let () = Typeops.check_hyps_inclusion env (GR.ConstRef c) cb.const_hyps in let u = EInstance.kind sigma u in let uctx = Declareops.constant_polymorphic_context cb in let csts = UVars.AbstractContext.instantiate u uctx in @@ -424,7 +425,7 @@ let type_of_constant env sigma (c,u) = let type_of_inductive env sigma (ind,u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in + let () = Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_inductive (specif,u) in let sigma = Evd.add_poly_constraints ~src:UState.Internal sigma csts in @@ -433,7 +434,7 @@ let type_of_inductive env sigma (ind,u) = let type_of_constructor env sigma ((ind,_ as ctor),u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = Reductionops.check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in + let () = Typeops.check_hyps_inclusion env (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in let sigma = Evd.add_poly_constraints ~src:UState.Internal sigma csts in diff --git a/test-suite/bugs/bug_11487.v b/test-suite/bugs/bug_11487.v new file mode 100644 index 000000000000..886009670efc --- /dev/null +++ b/test-suite/bugs/bug_11487.v @@ -0,0 +1,16 @@ +Parameter parameters: Type. +Parameter mem: parameters -> Type. +Parameter rel: forall {p: parameters}, mem p -> mem p -> Prop. + +Section Foo. + Context (p: parameters). + + Lemma Proper_load: forall (m: mem p), rel m m. Admitted. + + Goal forall (p: parameters) (m: mem p), rel m m. + Proof. + clear p. + intros p m. + Fail Check Proper_load. + Abort. +End Foo. diff --git a/test-suite/bugs/bug_20847_1.v b/test-suite/bugs/bug_20847_1.v new file mode 100644 index 000000000000..0937bed6a388 --- /dev/null +++ b/test-suite/bugs/bug_20847_1.v @@ -0,0 +1,18 @@ +(* #20847 is about secvars not getting renamed when pushing rel to + named. + + This test checks that clearing a secvar and renaming some other var + to reuse the secvar name is correctly handled (which seems + necessary to handle renaming secvars in the future). *) +Section C. + Variable n : nat. + + Definition d : n = n := eq_refl. + + Lemma l : n = n. + Proof. + revert n; intros []; [ reflexivity | ]. + apply eq_S. Fail apply d. + Fail Qed. + Abort. +End C. From 0c35e6bbd167b0b1d266126135338d5afbe364b5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 30 Apr 2026 15:42:41 +0200 Subject: [PATCH 03/17] Error instead of renaming section variable mentioned through a global Fix #12304 --- engine/evarutil.mli | 2 + pretyping/evarsolve.ml | 3 +- tactics/hints.ml | 1 + tactics/tactics.ml | 84 ++++++++++++++++++++++++++++++------- test-suite/bugs/bug_12304.v | 11 +++++ 5 files changed, 85 insertions(+), 16 deletions(-) create mode 100644 test-suite/bugs/bug_12304.v diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 75f9ac93240b..3aa80e258cc7 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -198,6 +198,8 @@ type unification_pb = conv_pb * env * constr * constr Put it at the end of the list if [tail] is true, by default it is false. *) val add_unification_pb : ?tail:bool -> unification_pb -> evar_map -> evar_map +val vars_of_global : env -> evar_map -> GlobRef.t -> Id.Set.t + (** {6 Removing hyps in evars'context} raise OccurHypInSimpleClause if the removal breaks dependencies *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 5e07133d88d1..fc3ec8b698e1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -568,7 +568,8 @@ let free_vars_and_rels_up_alias_expansion env sigma aliases c = | Some (RelAlias n) -> if n >= depth+1 then fv_rels := Int.Set.add (n-depth) !fv_rels | None -> frec (aliases,depth) c end | Const _ | Ind _ | Construct _ -> - fv_ids := Id.Set.union (vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids + (* XXX should be Evarutil.vars_of_global to handle abstracted constants? *) + fv_ids := Id.Set.union (Environ.vars_of_global env (fst @@ EConstr.destRef sigma c)) !fv_ids | _ -> iter_with_full_binders env sigma (fun d (aliases,depth) -> (extend_alias sigma d aliases,depth+1)) diff --git a/tactics/hints.ml b/tactics/hints.ml index 540f435732d8..752bdfdda477 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -897,6 +897,7 @@ let with_uid c = { obj = c; uid = fresh_key () } let secvars_of_idset s = Id.Set.fold (fun id p -> + (* XXX how can vars_of_global return non secvars? *) if is_section_variable (Global.env ()) id then Id.Pred.add id p else p) s Id.Pred.empty diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 61db30f713cf..7502ca6fd4b9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -217,6 +217,74 @@ let move_hyp id dest = end end +let error_renaming_implicit_dependency ?loc env where ids gr = + CErrors.user_err ?loc @@ + fmt "Cannot rename section variable %t@ because it is used implicitly through %t@ in %t." + (fun () -> Id.print (Id.Set.choose ids)) + (fun () -> pr_global_env env gr) + (fun () -> match where with + | None -> str "the conclusion" + | Some h -> fmt "hypothesis %t" (fun () -> Id.print h)) + +let check_renaming ~src ~dst env sigma concl = + let sign = named_context_val env in + (* Check that we do not mess variables *) + let vars = ids_of_named_context_val sign in + let () = + if not (Id.Set.subset src vars) then + let hyp = Id.Set.choose (Id.Set.diff src vars) in + raise (RefinerError (env, sigma, NoSuchHyp hyp)) + in + let mods = Id.Set.diff vars src in + let () = + try + let elt = Id.Set.choose (Id.Set.inter dst mods) in + TacticErrors.already_used elt + with Not_found -> () + in + let secvars = + Id.Set.filter (fun id -> + match var_status id env with + | SecVar -> true + | ProofVar -> false) + src + in + let checked = ref GlobRef.Set_env.empty in + let check_constr where c = + let rec aux c = + match EConstr.destRef sigma c with + | VarRef _, _ -> + (* we only refuse implicit dependencies, because they can't be substituted *) + () + | gr, _ -> + if GlobRef.Set_env.mem gr !checked then () + else begin + let deps = Evarutil.vars_of_global env sigma gr in + let bad = Id.Set.inter deps secvars in + let () = + if not @@ Id.Set.is_empty bad then + error_renaming_implicit_dependency env where bad gr + in + checked := GlobRef.Set_env.add gr !checked + end + | exception DestKO -> EConstr.iter sigma aux c + in + aux c + in + let () = + if Id.Set.is_empty secvars then + (* not renaming any secvars -> no problem *) + () + else + let () = check_constr None concl in + let () = + List.iter (fun d -> NamedDecl.iter_constr (check_constr (Some (NamedDecl.get_id d))) d) + (named_context env) + in + () + in + () + let rename_hyp repl = let fold accu (src, dst) = match accu with | None -> None @@ -238,23 +306,9 @@ let rename_hyp repl = Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let sign = named_context_val env in let sigma = Proofview.Goal.sigma gl in let relevance = Proofview.Goal.relevance gl in - (* Check that we do not mess variables *) - let vars = ids_of_named_context_val sign in - let () = - if not (Id.Set.subset src vars) then - let hyp = Id.Set.choose (Id.Set.diff src vars) in - raise (RefinerError (env, sigma, NoSuchHyp hyp)) - in - let mods = Id.Set.diff vars src in - let () = - try - let elt = Id.Set.choose (Id.Set.inter dst mods) in - TacticErrors.already_used elt - with Not_found -> () - in + let () = check_renaming ~src ~dst env sigma concl in (* All is well *) let make_subst (src, dst) = (src, mkVar dst) in let subst = List.map make_subst repl in diff --git a/test-suite/bugs/bug_12304.v b/test-suite/bugs/bug_12304.v new file mode 100644 index 000000000000..2f2740ffe607 --- /dev/null +++ b/test-suite/bugs/bug_12304.v @@ -0,0 +1,11 @@ +Section S. +Variable a:nat. +Definition b:=a. +Goal b=b. +Proof. + Fail rename a into c. + generalize b. intros b. + rename a into c. + Fail unfold b. +Abort. +End S. From 9eef589f7467498b8c7705e9b1b2e116b0df6ca1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 4 May 2026 14:49:59 +0200 Subject: [PATCH 04/17] Tactics.clear handle unbound ids This is accessible through Ltac2 Std.clear which doesn't check the ids before sending to Tactics.clear, and through ltac1 by abusing bound values eg `Ltac foo := match goal with H : _ |- _ => clear H; clear H end` --- tactics/tactics.ml | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7502ca6fd4b9..0ad37135dc2e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -156,15 +156,25 @@ end let convert x y = convert_gen Conversion.CONV x y let convert_leq x y = convert_gen Conversion.CUMUL x y +(* this should be an error but random code relies on it, eg + "match goal with H : _ |- _ => destruct H; clear H end" *) +let warn_clear_nohyp = CWarnings.create ~name:"clear-no-such-hyp" ~category:CWarnings.CoreCategories.tactics + Pp.(fun id -> fmt "No such hypothesis: %t." (fun () -> Id.print id)) + let clear_gen fail = function | [] -> Proofview.tclUNIT () | ids -> Proofview.Goal.enter begin fun gl -> - let ids = List.fold_right Id.Set.add ids Id.Set.empty in - (* clear_hyps_in_evi does not require nf terms *) let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in + let add id acc = + if Environ.mem_named id env then Id.Set.add id acc + else + let () = warn_clear_nohyp id in + acc + in + let ids = List.fold_right add ids Id.Set.empty in let (sigma, hyps, concl) = try clear_hyps_in_evi env sigma (named_context_val env) concl ids with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal From 78b65e7d8c395799c8c5dea094d5f362dea5b1a5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 30 Apr 2026 17:11:08 +0200 Subject: [PATCH 05/17] Use variable status to decide if a variable is section variable Termops.is_section_variable is deprecated and a new API Termops.is_section_variable' is added because their types are the same but they need different env arguments so changing in place would be too footgunny. ssr still uses the old "is it in global env" because IDK what it is doing. Fix #18858 --- engine/evarutil.ml | 52 +++++++----------- engine/evarutil.mli | 18 ++----- engine/namegen.ml | 8 +-- engine/termops.ml | 16 ++++-- engine/termops.mli | 9 +++- .../funind/functional_principles_proofs.ml | 2 +- plugins/funind/glob_termops.ml | 3 +- plugins/ltac/leminv.ml | 3 +- plugins/ltac2/tac2tactics.ml | 2 +- plugins/ssr/ssrcommon.ml | 2 +- plugins/ssrmatching/ssrmatching.ml | 2 + pretyping/cases.ml | 53 ++++++++----------- pretyping/globEnv.ml | 16 +++--- pretyping/globEnv.mli | 9 ++-- pretyping/pretyping.ml | 33 +++++------- tactics/auto.ml | 4 +- tactics/class_tactics.ml | 1 + tactics/eClause.ml | 3 +- tactics/eauto.ml | 2 +- tactics/equality.ml | 2 +- tactics/generalize.ml | 9 ++-- tactics/hints.ml | 18 +++---- tactics/hints.mli | 2 +- tactics/induction.ml | 43 ++++++++------- test-suite/bugs/bug_18858.v | 9 ++++ test-suite/bugs/bug_21987_1.v | 16 ++++++ test-suite/bugs/bug_21987_2.v | 8 +++ test-suite/success/clear.v | 21 ++++++-- vernac/proof_using.ml | 3 +- vernac/vernacentries.ml | 2 +- 30 files changed, 194 insertions(+), 177 deletions(-) create mode 100644 test-suite/bugs/bug_18858.v create mode 100644 test-suite/bugs/bug_21987_1.v create mode 100644 test-suite/bugs/bug_21987_2.v diff --git a/engine/evarutil.ml b/engine/evarutil.ml index aa451c09b682..e51486d69b81 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -284,18 +284,7 @@ let update_var src tgt subst = let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in { subst with csubst_var; csubst_rev } -module VarSet = -struct - type t = Id.t -> bool - let empty _ = false - let full _ = true - let variables env id = is_section_variable env id -end - -type naming_mode = VarSet.t - let push_rel_decl_to_named_context - ~hypnaming sigma decl (ext : ext_named_context) = let open EConstr in let open Vars in @@ -327,7 +316,7 @@ let push_rel_decl_to_named_context in match extract_if_neq id na with | Some id0 -> - if hypnaming id0 then + if Id.Map.mem id0 ext.ext_ctx.env_named_map && is_section_variable_sign ext.ext_ctx id0 then (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where the new binder has name [id]. Which amounts to the same @@ -370,7 +359,7 @@ let ext_rev_subst { ext_subst = subst } id0 = let default_ext_instance { ext_subst = subst; ext_ctx = ctx } = csubst_instance subst (named_context_of_val ctx) -let push_rel_context_to_named_context ~hypnaming env sigma typ = +let push_rel_context_to_named_context env sigma typ = (* compute the instances relative to the named context and rel_context *) let open EConstr in let ctx = named_context_val env in @@ -384,15 +373,15 @@ let push_rel_context_to_named_context ~hypnaming env sigma typ = (* We do keep the instances corresponding to local definition (see above) *) let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = ctx } in let ext = - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (rel_context env) ~init in let inst = default_ext_instance ext in (ext.ext_ctx, csubst_subst sigma ext.ext_subst typ, inst, ext.ext_subst) -let ext_named_context_of_env ~hypnaming env sigma = +let ext_named_context_of_env env sigma = let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in let init = { ext_subst = empty_csubst; ext_avoid = avoid; ext_ctx = named_context_val env } in - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) (EConstr.rel_context env) ~init (*------------------------------------* @@ -409,13 +398,9 @@ let next_evar_name naming = match naming with (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming = IntroAnonymous) ?parent ?typeclass_candidate - ?rrpat ?hypnaming env evd typ = + ?rrpat env evd typ = let name = next_evar_name naming in - let hypnaming = match hypnaming with - | Some n -> n - | None -> VarSet.variables (Global.env ()) - in - let sign,typ',instance,subst = push_rel_context_to_named_context ~hypnaming env evd typ in + let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in let map c = csubst_subst evd subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -430,10 +415,10 @@ let new_evar ?src ?filter ?relevance ?abstract_arguments ?candidates ?(naming = ?typeclass_candidate in (evd, EConstr.mkEvar (evk, instance)) -let new_type_evar ?src ?filter ?naming ?hypnaming env evd rigid = +let new_type_evar ?src ?filter ?naming env evd rigid = let (evd', s) = new_sort_variable rigid evd in let relevance = EConstr.ESorts.relevance_of_sort s in - let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false ?hypnaming (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ~relevance ?naming ~typeclass_candidate:false (EConstr.mkSort s) in evd', (e, s) let new_Type ?(rigid=Evd.univ_flexible) evd = @@ -518,7 +503,7 @@ let check_vars env sigma ids c = in check_rec c -let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~global c = +let rec check_and_clear_in_constr env evdref err ids ~global c = (* returns a new constr where all the evars have been 'cleaned' (ie the hypotheses ids have been removed from the contexts of evars). [global] should be true iff there is some variable of [ids] which @@ -585,9 +570,10 @@ let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~globa let _nconcl : EConstr.t = try let nids = Id.Map.domain rids in - let global = Id.Set.exists is_section_variable nids in + let env = evar_filtered_env env evi in + let global = Id.Set.exists (is_section_variable' env) nids in let concl = evar_concl evi in - check_and_clear_in_constr ~is_section_variable env evdref (EvarTypingBreak ev) nids ~global concl + check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids ~global concl with ClearDependencyError (rid,err,where) -> raise (ClearDependencyError (Id.Map.find rid rids,err,where)) in @@ -599,22 +585,21 @@ let rec check_and_clear_in_constr ~is_section_variable env evdref err ids ~globa evdref := evd; Evd.existential_value !evdref ev - | _ -> EConstr.map !evdref (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) c + | _ -> EConstr.map !evdref (check_and_clear_in_constr env evdref err ids ~global) c let clear_hyps_in_evi_main env sigma hyps terms ids = (* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) let evdref = ref sigma in - let is_section_variable id = is_section_variable (Global.env ()) id in - let global = Id.Set.exists is_section_variable ids in + let global = Id.Set.exists (is_section_variable' env) ids in let terms = - List.map (check_and_clear_in_constr ~is_section_variable env evdref (OccurHypInSimpleClause None) ids ~global) terms in + List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids ~global) terms in let nhyps = let check_context status decl = let decl = EConstr.of_named_decl decl in let err = OccurHypInSimpleClause (Some (NamedDecl.get_id decl)) in - status, EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr ~is_section_variable env evdref err ids ~global) decl + status, EConstr.Unsafe.to_named_decl @@ NamedDecl.map_constr (check_and_clear_in_constr env evdref err ids ~global) decl in remove_hyps ids check_context hyps in @@ -622,8 +607,9 @@ let clear_hyps_in_evi_main env sigma hyps terms ids = let check_and_clear_in_constr env evd err ids c = let evdref = ref evd in + let global = Id.Set.exists (is_section_variable' env) ids in let _ : EConstr.constr = check_and_clear_in_constr - ~is_section_variable:(fun _ -> true) ~global:true + ~global env evdref err ids c in !evdref diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 3aa80e258cc7..b942316b5294 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -26,16 +26,6 @@ val new_meta : unit -> metavariable val next_evar_name : intro_pattern_naming_expr -> (Id.t * bool) option -module VarSet : -sig - type t - val empty : t - val full : t - val variables : Environ.env -> t -end - -type naming_mode = VarSet.t - val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?relevance:ERelevance.t -> @@ -44,7 +34,6 @@ val new_evar : ?parent:Evar.t -> ?typeclass_candidate:bool -> ?rrpat:bool -> - ?hypnaming:naming_mode -> env -> evar_map -> types -> evar_map * EConstr.t (** Alias of {!Evd.new_pure_evar} *) @@ -63,7 +52,6 @@ val new_pure_evar : val new_type_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:intro_pattern_naming_expr -> - ?hypnaming:naming_mode -> env -> evar_map -> rigid -> evar_map * (constr * ESorts.t) @@ -239,7 +227,7 @@ val csubst_subst : Evd.evar_map -> csubst -> constr -> constr type ext_named_context -val ext_named_context_of_env : hypnaming:naming_mode -> env -> evar_map -> ext_named_context +val ext_named_context_of_env : env -> evar_map -> ext_named_context val ext_named_context_val : ext_named_context -> named_context_val val ext_csubst : ext_named_context -> csubst @@ -248,10 +236,10 @@ val default_ext_instance : ext_named_context -> constr SList.t val ext_rev_subst : ext_named_context -> Id.t -> constr -val push_rel_decl_to_named_context : hypnaming:naming_mode -> +val push_rel_decl_to_named_context : evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : hypnaming:naming_mode -> +val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> named_context_val * types * constr SList.t * csubst diff --git a/engine/namegen.ml b/engine/namegen.ml index 5494bc998e47..524adcc47d1c 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -99,10 +99,6 @@ let is_constructor id = with Not_found -> false -let is_section_variable env id = - try let _ = Environ.lookup_named id env in true - with Not_found -> false - (**********************************************************************) (* Generating "intuitive" names from its type *) @@ -401,7 +397,7 @@ let next_name_away_in_cases_pattern gen sigma env_t na avoid = let next_ident_away_in_goal env id avoid = let id = if Id.Set.mem id avoid then restart_subscript id else id in - let bad id = Id.Set.mem id avoid || (is_global id && not (is_section_variable env id)) in + let bad id = Id.Set.mem id avoid || (is_global id && not (Environ.mem_named id env)) in next_ident_away_from id bad let next_name_away_in_goal (type a) (gen : a Generator.t) env na (avoid : a) = @@ -409,7 +405,7 @@ let next_name_away_in_goal (type a) (gen : a Generator.t) env na (avoid : a) = | Name id -> id | Anonymous -> default_non_dependent_ident in let id = if Generator.is_fresh gen id avoid then id else restart_subscript id in - let bad id = is_global id && not (is_section_variable env id) in + let bad id = is_global id && not (Environ.mem_named id env) in Generator.gen_ident ~filter:bad gen id avoid (* 3- Looks for next fresh name outside a list that is moreover valid diff --git a/engine/termops.ml b/engine/termops.ml index ad1f64cf9deb..54871eaace91 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1007,10 +1007,13 @@ let ids_of_context env = let names_of_rel_context env = List.map RelDecl.get_name (rel_context env) -(* XXX use var status (NOT IN THIS ENV) *) -let is_section_variable env id = - try let _ = Environ.lookup_named id env in true - with Not_found -> false +let is_section_variable_sign ?check sign id = + match Environ.var_status_ctxt ?check id sign with + | SecVar -> true + | ProofVar -> false + +let is_section_variable' ?check env id = + is_section_variable_sign ?check (Environ.named_context_val env) id let is_template_polymorphic_ref env sigma f = match EConstr.kind sigma f with @@ -1424,3 +1427,8 @@ and hash_branches bl = Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl end + +(* deprecated *) +let is_section_variable env id = + try let _ = Environ.lookup_named id env in true + with Not_found -> false diff --git a/engine/termops.mli b/engine/termops.mli index 7a107183fd72..e6badbac1940 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -206,8 +206,15 @@ val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) * containing a given set *) val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.t list -(** Test if an identifier is the basename of a global reference *) +(** This tests if the ident is known in the given env, intended to be used with the global env. *) val is_section_variable : env -> Id.t -> bool +[@@deprecated "Use is_section_variable' on the local env instead of is_section_variable on the global env."] + +(** Check if the ident has [SecVar] status in this enviroment. + By default [check=true] and produce anomaly if it is not bound. + If [check=false] returns [false] if it is not bound. *) +val is_section_variable_sign : ?check:bool -> Environ.named_context_val -> Id.t -> bool +val is_section_variable' : ?check:bool -> env -> Id.t -> bool val is_template_polymorphic_ref : env -> Evd.evar_map -> constr -> bool val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 96dc5ee2aa4a..6eb38126f814 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -800,7 +800,7 @@ let generalize_non_dep hyp = Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env sigma hyp) keep || Termops.occur_var env sigma hyp hyp_typ - || Termops.is_section_variable (Global.env ()) hyp + || Termops.is_section_variable' env hyp (* should be dangerous *) then (clear, decl :: keep) else (hyp :: clear, keep)) diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4809a1ef05e1..623e3df74438 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -589,8 +589,7 @@ let resolve_and_replace_implicits exptyp env sigma rt = undeclared_evars_rr = false; unconstrained_sorts = false; } in - let hypnaming = Evarutil.VarSet.variables (Global.env ()) in - let genv = GlobEnv.make ~hypnaming env sigma Glob_ops.empty_lvar in + let genv = GlobEnv.make env sigma Glob_ops.empty_lvar in let pretyper = { default_pretyper with pretype_hole; pretype_type } in let sigma', _ = eval_pretyper pretyper ~flags:pretype_flags (Some exptyp) genv sigma rt in solve_remaining_evars flags env ~initial:sigma sigma' diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml index 2a7a7d1038ee..11e896c380d6 100644 --- a/plugins/ltac/leminv.ml +++ b/plugins/ltac/leminv.ml @@ -200,11 +200,10 @@ let inversion_scheme ~name ~poly env sigma t sort dep_option inv_op = let pf = Proof.start ~name ~poly (Evd.from_ustate (ustate sigma)) [invEnv,invGoal] in let pf, _, () = Proof.run_tactic env (tclTHEN intro (onLastHypId inv_op)) pf in let pfterm = List.hd (Proof.partial_proof pf) in - let global_named_context = Global.named_context_val () in let ownSign = ref begin fold_named_context (fun env status d sign -> - if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign + if status = SecVar then sign else Context.Named.add d sign) invEnv ~init:Context.Named.empty end in diff --git a/plugins/ltac2/tac2tactics.ml b/plugins/ltac2/tac2tactics.ml index 29e79d142628..5efd07b530bc 100644 --- a/plugins/ltac2/tac2tactics.ml +++ b/plugins/ltac2/tac2tactics.ml @@ -447,7 +447,7 @@ let wrap_tactic_call f = let open Proofview.Notations in let wrapf ~env ~carrier ~lhs ~rel = Proofview.tclEVARMAP >>= fun sigma -> - let ectx = ext_named_context_of_env ~hypnaming:Evarutil.VarSet.empty env sigma in + let ectx = ext_named_context_of_env env sigma in let subst = ext_csubst ectx in let carriern = Evarutil.csubst_subst sigma subst carrier in let lhsn = Evarutil.csubst_subst sigma subst lhs in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 21224a91bfec..e79cb3d6be9c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -47,7 +47,7 @@ let hyp_id (SsrHyp (_, id)) = id let hyp_err ?loc msg id = CErrors.user_err ?loc Pp.(str msg ++ Id.print id) -let not_section_id id = not (Termops.is_section_variable (Global.env ()) id) +let not_section_id id = not (Termops.is_section_variable (Global.env ()) id) [@@warning "-3"] let hyps_ids = List.map hyp_id diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 93881ab8f8a3..866e2d65d057 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1166,6 +1166,8 @@ let thin id sigma goal = let cl = Evd.evar_concl evi in let relevance = Evd.evar_relevance evi in let ans = + (* Why can this get called with an unknown id? *) + if not @@ Environ.mem_named id env then Some (sigma, Environ.named_context_val env, cl) else try Some (Evarutil.clear_hyps_in_evi env sigma (Environ.named_context_val env) cl ids) with Evarutil.ClearDependencyError _ -> None in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 36f2de210cb7..cf314eaa01f5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -504,11 +504,10 @@ let remove_current_pattern eqn = | [] -> anomaly (Pp.str "Empty list of patterns.") let push_current_pattern ~program_mode sigma (cur,ty) eqn = - let hypnaming = VarSet.variables (Global.env ()) in match eqn.patterns with | pat::pats -> let r = ERelevance.relevant in (* TODO relevance *) - let _,rhs_env = push_rel ~hypnaming sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in + let _,rhs_env = push_rel sigma (LocalDef (make_annot (alias_of_pat pat) r,cur,ty)) eqn.rhs.rhs_env in { eqn with rhs = { eqn.rhs with rhs_env = rhs_env }; patterns = pats } @@ -860,9 +859,9 @@ let recover_and_adjust_alias_names (_,avoid) names sign = in List.split (aux (names,sign)) -let push_rels_eqn ~hypnaming sigma sign eqn = +let push_rels_eqn sigma sign eqn = {eqn with - rhs = {eqn.rhs with rhs_env = snd (push_rel_context ~hypnaming sigma sign eqn.rhs.rhs_env) } } + rhs = {eqn.rhs with rhs_env = snd (push_rel_context sigma sign eqn.rhs.rhs_env) } } let push_rels_eqn_with_names sigma sign eqn = let subpats = List.rev (List.firstn (List.length sign) eqn.patterns) in @@ -870,12 +869,12 @@ let push_rels_eqn_with_names sigma sign eqn = let sign = recover_initial_subpattern_names subpatnames sign in push_rels_eqn sigma sign eqn -let push_generalized_decl_eqn ~hypnaming env sigma n decl eqn = +let push_generalized_decl_eqn env sigma n decl eqn = match RelDecl.get_name decl with | Anonymous -> - push_rels_eqn ~hypnaming sigma [decl] eqn + push_rels_eqn sigma [decl] eqn | Name _ -> - push_rels_eqn ~hypnaming sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn + push_rels_eqn sigma [RelDecl.set_name (RelDecl.get_name (Environ.lookup_rel n !!(eqn.rhs.rhs_env))) decl] eqn let drop_alias_eqn eqn = { eqn with alias_stack = List.tl eqn.alias_stack } @@ -1356,8 +1355,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname) let typs' = List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 typs in - let hypnaming = VarSet.variables (Global.env ()) in - let typs,extenv = push_rel_context ~hypnaming sigma typs pb.env in + let typs,extenv = push_rel_context sigma typs pb.env in let typs' = List.map (fun (c,d) -> @@ -1436,7 +1434,7 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname) tomatch = tomatch; pred = pred; history = history; - mat = List.map (push_rels_eqn_with_names ~hypnaming sigma typs) submat } + mat = List.map (push_rels_eqn_with_names sigma typs) submat } (********************************************************************** INVARIANT: @@ -1452,7 +1450,6 @@ let build_branch ~program_mode initial current realargs deps (realnames,curname) (**********************************************************************) (* Main compiling descent *) let compile ~program_mode sigma pb = - let hypnaming = VarSet.variables (Global.env ()) in let rec compile sigma pb = match pb.tomatch with | Pushed cur :: rest -> match_current sigma { pb with tomatch = rest } cur @@ -1519,7 +1516,7 @@ let compile ~program_mode sigma pb = let env = Name.fold_left (fun env id -> hide_variable env id) pb.env na in let pb = { pb with - env = snd (push_rel ~hypnaming sigma (LocalDef (annotR na,current,ty)) env); + env = snd (push_rel sigma (LocalDef (annotR na,current,ty)) env); tomatch = tomatch; pred = lift_predicate 1 pred tomatch; history = pop_history pb.history; @@ -1556,9 +1553,9 @@ let compile ~program_mode sigma pb = and compile_generalization sigma pb i d rest = let pb = { pb with - env = snd (push_rel ~hypnaming sigma d pb.env); + env = snd (push_rel sigma d pb.env); tomatch = rest; - mat = List.map (push_generalized_decl_eqn ~hypnaming pb.env sigma i d) pb.mat } in + mat = List.map (push_generalized_decl_eqn pb.env sigma i d) pb.mat } in let used, sigma, j = compile sigma pb in used, sigma, { uj_val = mkLambda_or_LetIn d j.uj_val; uj_type = mkProd_wo_LetIn d j.uj_type } @@ -1572,11 +1569,11 @@ let compile ~program_mode sigma pb = let alias = LocalDef (make_annot na r,c,t) in let pb = { pb with - env = snd (push_rel ~hypnaming sigma alias pb.env); + env = snd (push_rel sigma alias pb.env); tomatch = lift_tomatch_stack 1 rest; pred = lift_predicate 1 pb.pred pb.tomatch; history = pop_history_pattern pb.history; - mat = List.map (push_alias_eqn ~hypnaming sigma alias) pb.mat } in + mat = List.map (push_alias_eqn sigma alias) pb.mat } in let used, sigma, j = compile sigma pb in used, sigma, { uj_val = if isRel sigma c || isVar sigma c || count_occurrences sigma (mkRel 1) j.uj_val <= 1 then @@ -1718,8 +1715,7 @@ let adjust_to_extended_env_and_remove_deps env extenv sigma subst t = (subst0, t0) let push_binder sigma d (k,env,subst) = - let hypnaming = VarSet.variables (Global.env ()) in - (k+1,snd (push_rel ~hypnaming sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst) + (k+1,snd (push_rel sigma d env),List.map (fun (na,u,d) -> (na,lift 1 u,d)) subst) let rec list_assoc_in_triple x = function [] -> raise Not_found @@ -1842,7 +1838,6 @@ let build_tycon ?loc env tycon_env s subst tycon extenv sigma t = *) let build_inversion_problem ~program_mode loc env sigma tms t = - let hypnaming = VarSet.variables (Global.env ()) in let make_patvar t (subst,avoid) = let id = next_name_away (named_hd !!env sigma t Anonymous) avoid in DAst.make @@ PatVar (Name id), ((id,t)::subst, Id.Set.add id avoid) in @@ -1867,14 +1862,14 @@ let build_inversion_problem ~program_mode loc env sigma tms t = let patl = pat :: List.rev patl in let patl,sign = recover_and_adjust_alias_names acc patl sign in let p = List.length patl in - let _,env' = push_rel_context ~hypnaming sigma sign env in + let _,env' = push_rel_context sigma sign env in let patl',acc_sign,acc = aux (n+p) env' (sign@acc_sign) tms acc in List.rev_append patl patl',acc_sign,acc | (t, NotInd (bo,typ)) :: tms -> let pat,acc = make_patvar t acc in let typ = lift n typ in let d = LocalAssum (annotR (alias_of_pat pat),typ) in - let patl,acc_sign,acc = aux (n+1) (snd (push_rel ~hypnaming sigma d env)) (d::acc_sign) tms acc in + let patl,acc_sign,acc = aux (n+1) (snd (push_rel sigma d env)) (d::acc_sign) tms acc in pat::patl,acc_sign,acc in let avoid0 = GlobEnv.vars_of_env env in (* [patl] is a list of patterns revealing the substructure of @@ -1892,7 +1887,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t = let decls = List.map_i (fun i d -> (mkRel i, map_constr (lift i) d)) 1 sign in - let _,pb_env = push_rel_context ~hypnaming sigma sign env in + let _,pb_env = push_rel_context sigma sign env in let decls = List.map (fun (c,d) -> (c,extract_inductive_data !!(pb_env) sigma d,d)) decls in @@ -2102,8 +2097,7 @@ let prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs ars in assert (len == 0); let p = predicate 0 c in - let hypnaming = VarSet.variables (Global.env ()) in - let arsign,env' = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in + let arsign,env' = List.fold_right_map (push_rel_context sigma) arsign env in try let sigma' = fst (Typing.type_of !!env' sigma p) in Some (sigma', p, arsign) with e when precatchable_exception e -> None @@ -2165,8 +2159,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty (* Some type annotation *) | Some rtntyp -> (* We extract the signature of the arity *) - let hypnaming = VarSet.variables (Global.env ()) in - let building_arsign,envar = List.fold_right_map (push_rel_context ~hypnaming sigma) arsign env in + let building_arsign,envar = List.fold_right_map (push_rel_context sigma) arsign env in let sigma, rtnsort = Evd.new_sort_variable univ_flexible sigma in let sigma, predcclj = typing_fun (Some (mkSort rtnsort)) envar sigma rtntyp in let check_elim_sort sigma squash = @@ -2420,7 +2413,6 @@ let build_ineqs env sigma prevpatterns curpats curpat_sign_len = let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = let i = ref 0 in - let hypnaming = VarSet.variables (Global.env ()) in let (sigma, x, y, z) = List.fold_left (fun (sigma, branches, eqns, prevpatterns) eqn -> @@ -2483,7 +2475,7 @@ let constrs_of_pats typing_fun env sigma eqns tomatchs sign neqs arity = let eqs_rels, arity = decompose_prod_n_decls sigma neqs arity in eqs_rels @ neqs_rels @ rhs_rels', arity in - let _,rhs_env = push_rel_context ~hypnaming sigma rhs_rels' env in + let _,rhs_env = push_rel_context sigma rhs_rels' env in let sigma, j = typing_fun (mk_tycon tycon) rhs_env sigma eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in @@ -2697,7 +2689,6 @@ let context_of_arsign l = let compile_program_cases ?loc style (typing_function, sigma) tycon env (predopt, tomatchl, eqns) = - let hypnaming = VarSet.variables (Global.env ()) in let typing_fun tycon env sigma = function | Some t -> typing_function tycon env sigma t | None -> coq_unit_judge !!env sigma in @@ -2710,7 +2701,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env let env, sigma, tomatchs = coerce_to_indtype ~program_mode:true typing_function env sigma matx tomatchl in let tycon = valcon_of_tycon tycon in let tomatchs, tomatchs_lets, tycon' = abstract_tomatch env sigma tomatchs tycon in - let _,env = push_rel_context ~hypnaming sigma tomatchs_lets env in + let _,env = push_rel_context sigma tomatchs_lets env in let len = List.length eqns in let sigma, sign, signlen, eqs, args = (* The arity signature *) @@ -2746,7 +2737,7 @@ let compile_program_cases ?loc style (typing_function, sigma) tycon env in let matx = List.rev matx in let _ = assert (Int.equal len (List.length lets)) in - let _,env = push_rel_context ~hypnaming sigma lets env in + let _,env = push_rel_context sigma lets env in let matx = List.map (fun eqn -> { eqn with rhs = { eqn.rhs with rhs_env = env } }) matx in let tomatchs = List.map (fun (x, y) -> lift len x, lift_tomatch_type len y) tomatchs in let args = List.rev_map (lift len) args in diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index fb2e18a34ab7..a2ab718571a4 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -38,8 +38,8 @@ type t = { lvar : ltac_var_map; } -let make ~hypnaming env sigma lvar = - let get_extra env sigma = ext_named_context_of_env ~hypnaming env sigma in +let make env sigma lvar = + let get_extra env sigma = ext_named_context_of_env env sigma in { static_env = env; renamed_env = env; @@ -65,33 +65,33 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id = let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) -let push_rel ~hypnaming sigma d env = +let push_rel sigma d env = let open Context.Rel.Declaration in let d' = map_name (ltac_interp_name env.lvar) d in let env = { static_env = push_rel d env.static_env; renamed_env = push_rel d' env.renamed_env; - extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra)); + extra = lazy (push_rel_decl_to_named_context sigma d' (Lazy.force env.extra)); lvar = env.lvar; } in d', env -let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env = +let push_rel_context ?(force_names=false) sigma ctx env = let open Context.Rel.Declaration in let ctx' = List.Smart.map (map_name (ltac_interp_name env.lvar)) ctx in let ctx' = if force_names then Namegen.name_context env.renamed_env sigma ctx' else ctx' in let env = { static_env = push_rel_context ctx env.static_env; renamed_env = push_rel_context ctx' env.renamed_env; - extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra)); + extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context sigma d acc) ctx' (Lazy.force env.extra)); lvar = env.lvar; } in ctx', env -let push_rec_types ~hypnaming sigma (lna,typarray) env = +let push_rec_types sigma (lna,typarray) env = let open Context.Rel.Declaration in let ctxt = Array.map2_i (fun i na t -> Context.Rel.Declaration.LocalAssum (na, lift i t)) lna typarray in - let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e ~hypnaming in (e,d)) env ctxt in + let env,ctx = Array.fold_left_map (fun e assum -> let (d,e) = push_rel sigma assum e in (e,d)) env ctxt in Array.map get_annot ctx, env let new_evar env sigma ?src ?rrpat ?(naming = Namegen.IntroAnonymous) ?relevance typ = diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 2f2f4998171f..44065277f8c8 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -13,7 +13,6 @@ open Environ open Evd open EConstr open Ltac_pretype -open Evarutil (** Type of environment extended with naming and ltac interpretation data *) @@ -41,7 +40,7 @@ val register_constr_interp0 : (** Build a pretyping environment from an ltac environment *) -val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t +val make : env -> evar_map -> ltac_var_map -> t (** Export the underlying environment *) @@ -53,9 +52,9 @@ val vars_of_env : t -> Id.Set.t (** Push to the environment, returning the declaration(s) with interpreted names *) -val push_rel : hypnaming:naming_mode -> evar_map -> rel_declaration -> t -> rel_declaration * t -val push_rel_context : hypnaming:naming_mode -> ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t -val push_rec_types : hypnaming:naming_mode -> evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t +val push_rel : evar_map -> rel_declaration -> t -> rel_declaration * t +val push_rel_context : ?force_names:bool -> evar_map -> rel_context -> t -> rel_context * t +val push_rec_types : evar_map -> Name.t EConstr.binder_annot array * constr array -> t -> Name.t EConstr.binder_annot array * t (** Declare an evar using renaming information *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2faea419716a..648d6e9c6990 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -795,27 +795,26 @@ struct let open Context.Rel.Declaration in let pretype tycon env sigma c = eval_pretyper self ~flags tycon env sigma c in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in - let hypnaming = VarSet.variables (Global.env ()) in let rec type_bl env sigma ctxt = function | [] -> sigma, ctxt | (na,_,bk,None,ty)::bl -> let sigma, ty' = pretype_type empty_valcon env sigma ty in let rty' = ESorts.relevance_of_sort ty'.utj_type in let dcl = LocalAssum (make_annot na rty', ty'.utj_val) in - let dcl', env = push_rel ~hypnaming sigma dcl env in + let dcl', env = push_rel sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl | (na,_,bk,Some bd,ty)::bl -> let sigma, ty' = pretype_type empty_valcon env sigma ty in let rty' = ESorts.relevance_of_sort ty'.utj_type in let sigma, bd' = pretype (mk_tycon ty'.utj_val) env sigma bd in let dcl = LocalDef (make_annot na rty', bd'.uj_val, ty'.utj_val) in - let dcl', env = push_rel ~hypnaming sigma dcl env in + let dcl', env = push_rel sigma dcl env in type_bl env sigma (Context.Rel.add dcl' ctxt) bl in let sigma, ctxtv = Array.fold_left_map (fun sigma -> type_bl env sigma Context.Rel.empty) sigma bl in let sigma, larj = Array.fold_left2_map (fun sigma e ar -> - pretype_type empty_valcon (snd (push_rel_context ~hypnaming sigma e env)) sigma ar) + pretype_type empty_valcon (snd (push_rel_context sigma e env)) sigma ar) sigma ctxtv lar in let lara = Array.map (fun a -> a.utj_val) larj in let ftys = Array.map2 (fun e a -> it_mkProd_or_LetIn a e) ctxtv lara in @@ -839,7 +838,7 @@ struct names ftys in (* Note: bodies are not used by push_rec_types, so [||] is safe *) - let names,newenv = push_rec_types ~hypnaming sigma (names,ftys) env in + let names,newenv = push_rec_types sigma (names,ftys) env in let sigma, vdefj = Array.fold_left2_map_i (fun i sigma ctxt def -> @@ -848,7 +847,7 @@ struct let (ctxt,ty) = decompose_prod_n_decls sigma (Context.Rel.length ctxt) (lift nbfix ftys.(i)) in - let ctxt,nenv = push_rel_context ~hypnaming sigma ctxt newenv in + let ctxt,nenv = push_rel_context sigma ctxt newenv in let sigma, j = pretype (mk_tycon ty) nenv sigma def in sigma, { uj_val = it_mkLambda_or_LetIn j.uj_val ctxt; uj_type = it_mkProd_or_LetIn j.uj_type ctxt }) @@ -1251,8 +1250,7 @@ struct let sigma, j = eval_type_pretyper self ~flags dom_valcon env sigma c1 in let name = {binder_name=name; binder_relevance=ESorts.relevance_of_sort j.utj_type} in let var = LocalAssum (name, j.utj_val) in - let hypnaming = VarSet.variables (Global.env ()) in - let var',env' = push_rel ~hypnaming sigma var env in + let var',env' = push_rel sigma var env in let sigma, j' = eval_pretyper self ~flags rng env' sigma c2 in let name = get_name var' in let resj = judge_of_abstraction !!env sigma (orelse_name name name') j j' in @@ -1263,7 +1261,6 @@ struct let open Context.Rel.Declaration in let pretype_type tycon env sigma c = eval_type_pretyper self ~flags tycon env sigma c in let sigma, j = pretype_type empty_valcon env sigma c1 in - let hypnaming = VarSet.variables (Global.env ()) in let sigma, name, j' = match name with | Anonymous -> let sigma, j = pretype_type empty_valcon env sigma c2 in @@ -1271,7 +1268,7 @@ struct | Name _ -> let r = ESorts.relevance_of_sort j.utj_type in let var = LocalAssum (make_annot name r, j.utj_val) in - let var, env' = push_rel ~hypnaming sigma var env in + let var, env' = push_rel sigma var env in let sigma, c2_j = pretype_type empty_valcon env' sigma c2 in sigma, get_name var, c2_j in @@ -1302,8 +1299,7 @@ struct let r = Retyping.relevance_of_term !!env sigma j.uj_val in let var = LocalDef (make_annot name r, j.uj_val, t) in let tycon = lift_tycon 1 tycon in - let hypnaming = VarSet.variables (Global.env ()) in - let var, env = push_rel ~hypnaming sigma var env in + let var, env = push_rel sigma var env in let sigma, j' = pretype tycon env sigma c2 in let name = get_name var in sigma, { uj_val = mkLetIn (make_annot name r, j.uj_val, t, j'.uj_val) ; @@ -1348,8 +1344,7 @@ struct | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in let fsign = Context.Rel.map (whd_betaiota !!env sigma) fsign in - let hypnaming = VarSet.variables (Global.env ()) in - let fsign,env_f = push_rel_context ~hypnaming sigma fsign env in + let fsign,env_f = push_rel_context sigma fsign env in let obj sigma indt rci p v f = if not record then let f = it_mkLambda_or_LetIn f fsign in @@ -1366,7 +1361,7 @@ struct let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in let nar = List.length arsgn in - let psign',env_p = push_rel_context ~hypnaming ~force_names:true sigma psign predenv in + let psign',env_p = push_rel_context ~force_names:true sigma psign predenv in (match po with | Some p -> let sigma, pj = pretype_type empty_valcon env_p sigma p in @@ -1431,8 +1426,7 @@ struct let indt = build_dependent_inductive !!env indf in let psign = LocalAssum (make_annot na indr, indt) :: arsgn in (* For locating names in [po] *) let predenv = Cases.make_return_predicate_ltac_lvar env sigma na c cj.uj_val in - let hypnaming = VarSet.variables (Global.env ()) in - let psign,env_p = push_rel_context ~hypnaming sigma psign predenv in + let psign,env_p = push_rel_context sigma psign predenv in let sigma, pred, p = match po with | Some p -> let sigma, pj = eval_type_pretyper self ~flags empty_valcon env_p sigma p in @@ -1457,7 +1451,7 @@ struct let csgn = List.map (set_name Anonymous) cs_args in - let _,env_c = push_rel_context ~hypnaming sigma csgn env in + let _,env_c = push_rel_context sigma csgn env in let sigma, bj = pretype (mk_tycon pi) env_c sigma b in sigma, it_mkLambda_or_LetIn bj.uj_val cs_args in let sigma, b1 = f sigma cstrs.(0) b1 in @@ -1675,8 +1669,7 @@ let ise_pretype_gen (flags : inference_flags) env sigma lvar kind c = | NoUseTC -> false | UseTC | UseTCForConv -> true } in - let hypnaming = VarSet.variables (Global.env ()) in - let env = GlobEnv.make ~hypnaming env sigma lvar in + let env = GlobEnv.make env sigma lvar in let sigma', c', c'_ty = match kind with | WithoutTypeConstraint -> let sigma, j = pretype ~flags:pretype_flags empty_tycon env sigma c in diff --git a/tactics/auto.ml b/tactics/auto.ml index 85ca53b315e9..a5089f9bfb4b 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -25,8 +25,8 @@ open Hints (**************************************************************************) let compute_secvars gl = - let hyps = Proofview.Goal.hyps gl in - secvars_of_hyps hyps + let env = Proofview.Goal.env gl in + secvars_of_hyps (Environ.named_context_val env) (* Tell auto not to reuse already instantiated metas in unification (for compatibility, since otherwise, apply succeeds more often). *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 8a46776ac73d..e90fe12f0ef3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -448,6 +448,7 @@ let make_hints env sigma (modes,st) only_classes = (fun _ status hyp hints -> let consider = not only_classes || + not (status = SecVar) || try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in (* Section variable, reindex only if the type changed *) not (EConstr.eq_constr sigma (EConstr.of_constr t) (NamedDecl.get_type hyp)) diff --git a/tactics/eClause.ml b/tactics/eClause.ml index 35a457dce869..6c735ca93b03 100644 --- a/tactics/eClause.ml +++ b/tactics/eClause.ml @@ -80,8 +80,7 @@ let make_evar_clause env sigma ?len t = let inst, ctx, args, subst = match inst with | None -> (* Dummy type *) - let hypnaming = VarSet.variables (Global.env ()) in - let ctx, _, args, subst = push_rel_context_to_named_context ~hypnaming env sigma mkProp in + let ctx, _, args, subst = push_rel_context_to_named_context env sigma mkProp in Some (ctx, args, subst), ctx, args, subst | Some (ctx, args, subst) -> inst, ctx, args, subst in diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2340da4f8b35..9ac982f17467 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -210,7 +210,7 @@ module Search = struct let concl = Proofview.Goal.concl gl in let hyps = EConstr.named_context env in let db = db env sigma in - let secvars = secvars_of_hyps hyps in + let secvars = secvars_of_hyps (Environ.named_context_val env) in let assumption_tacs = let mkdb env sigma = assert false in (* no goal can be generated *) let map_assum id = (false, mkdb, e_give_exact (mkVar id), lazy (str "exact" ++ spc () ++ Id.print id)) in diff --git a/tactics/equality.ml b/tactics/equality.ml index 59e7a64547ae..e50536e57768 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1849,7 +1849,7 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in - if is_section_variable (Global.env ()) x then + if is_section_variable' env x then check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end diff --git a/tactics/generalize.ml b/tactics/generalize.ml index 31460e3a7684..efabb5313b1d 100644 --- a/tactics/generalize.ml +++ b/tactics/generalize.ml @@ -152,7 +152,8 @@ let generalize_dep ?(with_let=false) c = let sigma = Proofview.Goal.sigma gl in let concl = Proofview.Goal.concl gl in let sign = named_context_val env in - let init_ids = ids_of_named_context (Global.named_context()) in + (* XXX avoid section variables still in env instead of all section variables? *) + let init_ids = Environ.ids_of_named_context_val (Global.named_context_val()) in let seek (d:named_declaration) (toquant:named_context) = if List.exists (fun d' -> occur_var_in_decl env sigma (NamedDecl.get_id d') d) toquant || dependent_in_decl sigma c d then @@ -161,10 +162,10 @@ let generalize_dep ?(with_let=false) c = toquant in let to_quantify = Context.Named.fold_outside seek (named_context_of_val sign) ~init:[] in let qhyps = List.map NamedDecl.get_id to_quantify in - let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in + let tothin = List.filter (fun id -> not (Id.Set.mem id init_ids)) qhyps in let tothin' = match EConstr.kind sigma c with - | Var id when mem_named_context_val id sign && not (Id.List.mem id init_ids) + | Var id when mem_named_context_val id sign && not (Id.Set.mem id init_ids) -> tothin@[id] | _ -> tothin in @@ -172,7 +173,7 @@ let generalize_dep ?(with_let=false) c = let is_var, body = match EConstr.kind sigma c with | Var id -> let body = NamedDecl.get_value (Tacmach.pf_get_hyp id gl) in - let is_var = Option.is_empty body && not (List.mem id init_ids) in + let is_var = Option.is_empty body && not (Id.Set.mem id init_ids) in if with_let then is_var, body else is_var, None | _ -> false, None in diff --git a/tactics/hints.ml b/tactics/hints.ml index 752bdfdda477..9d9bd3ff7869 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -77,14 +77,13 @@ let secvars_of_hyps hyps = let open Context.Named.Declaration in let pred, all = List.fold_left (fun (pred,all) decl -> - try let _ = Context.Named.lookup (get_id decl) hyps in - (* Approximation, it might be an hypothesis reintroduced with same name and unconvertible types, - we must allow it currently, as comparing the declarations for syntactic equality is too - strong a check (e.g. an unfold in a section variable would make it unusable). *) + if Termops.is_section_variable_sign ~check:false hyps (get_id decl) then (Id.Pred.add (get_id decl) pred, all) - with Not_found -> (pred, false)) + else (pred, false)) (Id.Pred.empty,true) secctx in + (* NB: this is not just [forall is_secvar hyps] because we need to + know if secvars have been cleaned *) if all then Id.Pred.full (* If the whole section context is available *) else pred @@ -895,15 +894,16 @@ let error_no_such_hint_database x = let with_uid c = { obj = c; uid = fresh_key () } -let secvars_of_idset s = +(* if [x] is a local variable sharing a name with a cleared section + variable, [secvars_of_global _ (VarRef x)] should return the empty set *) +let secvars_of_idset env s = Id.Set.fold (fun id p -> - (* XXX how can vars_of_global return non secvars? *) - if is_section_variable (Global.env ()) id then + if is_section_variable' env id then Id.Pred.add id p else p) s Id.Pred.empty let secvars_of_global env gr = - secvars_of_idset (vars_of_global env gr) + secvars_of_idset env (vars_of_global env gr) let fresh_global_hint env sigma gr = let (c, ctx) = UnivGen.fresh_global_instance env gr in diff --git a/tactics/hints.mli b/tactics/hints.mli index 568fb4cd754a..da7bdae78c6b 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -23,7 +23,7 @@ val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array type debug = Debug | Info | Off -val secvars_of_hyps : ('c, 't,'r) Context.Named.pt -> Id.Pred.t +val secvars_of_hyps : Environ.named_context_val -> Id.Pred.t val empty_hint_info : 'a Typeclasses.hint_info_gen diff --git a/tactics/induction.ml b/tactics/induction.ml index 02c5b6f75c67..a0ef78585cc2 100644 --- a/tactics/induction.ml +++ b/tactics/induction.ml @@ -1397,7 +1397,7 @@ let induction_gen ~clear_flag ~isrec ~with_evars elim let cls = Option.default allHypsAndConcl cls in let t = typ_of env evd c in let is_arg_pure_hyp = - isVar evd c && not (mem_named_context_val (destVar evd c) (Global.named_context_val ())) + isVar evd c && not (is_section_variable' env (destVar evd c)) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in @@ -1445,28 +1445,27 @@ let induction_gen_l isrec with_evars elim names lc = match l with | [] -> Proofview.tclUNIT () | c::l' -> - Proofview.tclEVARMAP >>= fun sigma -> + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in match EConstr.kind sigma c with - | Var id when not (mem_named_context_val id (Global.named_context_val ())) - && not with_evars -> - let () = newlc:= id::!newlc in - atomize_list l' - - | _ -> - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let sigma, t = Typing.type_of env sigma c in - let x = id_of_name_using_hdchar env sigma t Anonymous in - let id = new_fresh_id Id.Set.empty x gl in - let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in - let () = newlc:=id::!newlc in - Tacticals.tclTHENLIST [ - tclEVARS sigma; - Tactics.letin_tac None (Name id) c None allHypsAndConcl; - atomize_list newl'; - ] - end in + | Var id when not (is_section_variable' env id) + && not with_evars -> + let () = newlc:= id::!newlc in + atomize_list l' + + | _ -> + let sigma, t = Typing.type_of env sigma c in + let x = id_of_name_using_hdchar env sigma t Anonymous in + let id = new_fresh_id Id.Set.empty x gl in + let newl' = List.map (fun r -> replace_term sigma c (mkVar id) r) l' in + let () = newlc:=id::!newlc in + Tacticals.tclTHENLIST [ + tclEVARS sigma; + Tactics.letin_tac None (Name id) c None allHypsAndConcl; + atomize_list newl'; + ] + end in Tacticals.tclTHENLIST [ (atomize_list lc); diff --git a/test-suite/bugs/bug_18858.v b/test-suite/bugs/bug_18858.v new file mode 100644 index 000000000000..a2f6b4df79a0 --- /dev/null +++ b/test-suite/bugs/bug_18858.v @@ -0,0 +1,9 @@ +Section Test. + Context (H : True). + Goal True /\ True -> True. + Proof. + intros H'. rename H into H0. rename H' into H. + repeat match goal with [ H : _ /\ _ |- _ ] => destruct H end. (* fails with timeout because [H] is not cleared by [destruct] *) + trivial. + Qed. +End Test. diff --git a/test-suite/bugs/bug_21987_1.v b/test-suite/bugs/bug_21987_1.v new file mode 100644 index 000000000000..c67a26644c26 --- /dev/null +++ b/test-suite/bugs/bug_21987_1.v @@ -0,0 +1,16 @@ + +Axiom t : Type -> Type. + +Section S. + Variable elt : Type. + + Lemma t_ind : + forall P : t elt -> Type, + forall m, P m. + Proof. + Admitted. + + Goal forall m : t elt, m = m. + induction m using t_ind. + Qed. +End S. diff --git a/test-suite/bugs/bug_21987_2.v b/test-suite/bugs/bug_21987_2.v new file mode 100644 index 000000000000..557bef096d3d --- /dev/null +++ b/test-suite/bugs/bug_21987_2.v @@ -0,0 +1,8 @@ +Goal True /\ True -> True. +Proof. + intros H. + match goal with + | H : _ /\ _ |- _ => + destruct H as [H1 H2]; try clear H + end. +Abort. diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 03034cf1305e..ad093ef6b9bb 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -15,19 +15,34 @@ Qed. Class A. +Class B := BB : A. + Section Foo. Variable a : A. Goal A. solve [typeclasses eauto]. - Undo 1. + Qed. + + Goal A. clear a. - try typeclasses eauto. + Fail solve [ typeclasses eauto ]. assert(a:=Build_A). solve [ typeclasses eauto ]. - Undo 2. + Qed. + + Goal A. + clear a. assert(b:=Build_A). solve [ typeclasses eauto ]. Qed. + + Instance myb : B := a. + + Goal B. + clear a. + assert(a:=Build_A). + Fail solve [typeclasses eauto]. + Abort. End Foo. diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index c8f7bc6cc4bb..c9d0366ab786 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -109,7 +109,8 @@ let definition_using env evd ~fixnames ~using ~terms = let name_set id expr = if Id.equal id all_collection_id then err_redefine_all_collection (); if is_known_name id then warn_redefine_collection id; - if Termops.is_section_variable (Global.env ()) id then warn_variable_shadowing id; + (* but we won't warn if id gets declared as a section variable later *) + if Environ.mem_named id (Global.env ()) then warn_variable_shadowing id; known_names := (id,expr) :: !known_names let minimize_hyps env ids = diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7d2fea021b73..86adb56b5020 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -823,7 +823,7 @@ let vernac_enable_notation ~module_local on rule interp flags scope = let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) - if Termops.is_section_variable (Global.env ()) id || + if Environ.mem_named id (Global.env ()) || locality <> Discharge && Nametab.exists_cci (Lib.make_path id) || locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id) then From 44ee3d29f17f88a67519fd11cc5de9412c0a41f0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 May 2026 16:55:30 +0200 Subject: [PATCH 06/17] changelog for section variable status tracking --- .../04-tactics/21987-context-secvar-Changed.rst | 5 +++++ .../04-tactics/21987-context-secvar-Fixed.rst | 11 +++++++++++ 2 files changed, 16 insertions(+) create mode 100644 doc/changelog/04-tactics/21987-context-secvar-Changed.rst create mode 100644 doc/changelog/04-tactics/21987-context-secvar-Fixed.rst diff --git a/doc/changelog/04-tactics/21987-context-secvar-Changed.rst b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst new file mode 100644 index 000000000000..5f8714bf4b94 --- /dev/null +++ b/doc/changelog/04-tactics/21987-context-secvar-Changed.rst @@ -0,0 +1,5 @@ +- **Changed:** + :tacn:`clear` checks that identifiers are bound even when they are ltac variables + (typically in `match goal with H : _ |- _ => foo H; clear H end`, `clear` now fails if `foo` cleared H where before it would succeed without doing anything) + (`#21987 `_, + by Gaëtan Gilbert). diff --git a/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst new file mode 100644 index 000000000000..58be0ef1c22a --- /dev/null +++ b/doc/changelog/04-tactics/21987-context-secvar-Fixed.rst @@ -0,0 +1,11 @@ +- **Fixed:** + the proof engine now keeps track of which hypotheses are section variables + instead of assuming that a variable sharing a name with a section variable is a section variable. + In particular :tacn:`destruct` now clears non-section-variable variables which share a name with a section variable. + Note that modifying a section variable (e.g. with `apply in`) makes it a non-section-variable + (`#21987 `_, + fixes `#18858 `_ + and `#12304 `_ + and `#11487 `_ + and `#6773 `_, + by Gaëtan Gilbert). From d52593d7e8248cff18242392251a309e096e9141 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 May 2026 16:58:24 +0200 Subject: [PATCH 07/17] better error message for ReferenceVariables for secvar status mismatch --- vernac/himsg.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 1041122c1307..6e132ff6a603 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -230,9 +230,11 @@ let explain_bad_assumption env sigma j = brk(1,1) ++ pc ++ spc () ++ str "of type" ++ spc () ++ pt ++ spc () ++ str "because this term is not a type." -let explain_reference_variables sigma id c = - pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++ - strbrk " which is not declared in the context." +let explain_reference_variables env sigma id c = + pr_global c ++ strbrk " depends on the section variable " ++ Id.print id ++ + if Environ.mem_named id env then + strbrk " but " ++ Id.print id ++ strbrk " in the current context does not refer to the section variable of the same name." + else strbrk " which is not declared in the current context." let explain_elim_arity env sigma ind c okinds = let open EConstr in @@ -1008,7 +1010,7 @@ let explain_type_error env sigma err = | BadAssumption c -> explain_bad_assumption env sigma c | ReferenceVariables (id,c) -> - explain_reference_variables sigma id c + explain_reference_variables env sigma id c | ElimArity (ind, c, okinds) -> explain_elim_arity env sigma ind (Some c) okinds | CaseNotInductive cj -> From 4efd00c331afddd1f48deb9a17df413706cc5120 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 May 2026 17:11:27 +0200 Subject: [PATCH 08/17] slightly streamline pr_context_of code --- printing/printer.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/printing/printer.ml b/printing/printer.ml index 6719789f7bee..4aa208ab0a5b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -521,9 +521,9 @@ let { Goptions.get = print_hyps_limit } = ~value:None () -let pr_context_of ?flags env sigma = match print_hyps_limit () with - | None -> hv 0 (pr_context_limit_compact ?flags env sigma) - | Some n -> hv 0 (pr_context_limit_compact ~n ?flags env sigma) +let pr_context_of ?flags env sigma = + let n = print_hyps_limit () in + hv 0 (pr_context_limit_compact ?n ?flags env sigma) (* display goal parts (Proof mode) *) From 8d6ddc01cdab227c09e723328c05fb25abae1cb5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 May 2026 17:29:42 +0200 Subject: [PATCH 09/17] Move CompactedDecl to ppconstr --- engine/eConstr.ml | 2 -- engine/eConstr.mli | 2 -- engine/termops.ml | 23 ----------------------- engine/termops.mli | 1 - ide/rocqide/idetop.ml | 2 +- kernel/constr.ml | 2 -- kernel/constr.mli | 2 -- kernel/context.ml | 29 ----------------------------- kernel/context.mli | 17 ----------------- printing/ppconstr.ml | 39 +++++++++++++++++++++++++++++++++++++++ printing/ppconstr.mli | 14 ++++++++++++++ printing/printer.ml | 29 ++++++++++++----------------- printing/printer.mli | 4 +--- printing/proof_diffs.ml | 11 ++--------- 14 files changed, 69 insertions(+), 108 deletions(-) diff --git a/engine/eConstr.ml b/engine/eConstr.ml index c1b629fbc274..5f73db590b59 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -171,9 +171,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = (types, ESorts.t) Environ.punsafe_type_judgment type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt -type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt type named_context = (constr, types, ERelevance.t) Context.Named.pt -type compacted_context = compacted_declaration list type rel_context = (constr, types, ERelevance.t) Context.Rel.pt type 'a binder_annot = ('a, ERelevance.t) Context.pbinder_annot diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 0b7cec293478..6d2cab493c23 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -93,9 +93,7 @@ type unsafe_judgment = (constr, types) Environ.punsafe_judgment type unsafe_type_judgment = (types, Evd.esorts) Environ.punsafe_type_judgment type named_declaration = (constr, types, ERelevance.t) Context.Named.Declaration.pt type rel_declaration = (constr, types, ERelevance.t) Context.Rel.Declaration.pt -type compacted_declaration = (constr, types, ERelevance.t) Context.Compacted.Declaration.pt type named_context = (constr, types, ERelevance.t) Context.Named.pt -type compacted_context = compacted_declaration list type rel_context = (constr, types, ERelevance.t) Context.Rel.pt type 'a binder_annot = ('a,ERelevance.t) Context.pbinder_annot diff --git a/engine/termops.ml b/engine/termops.ml index 54871eaace91..c9b8643fadd7 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -22,7 +22,6 @@ open Environ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -module CompactedDecl = Context.Compacted.Declaration module Internal = struct @@ -1182,28 +1181,6 @@ let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init let mem_named_context_val id ctxt = try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false -let compact_named_context sigma sign = - let compact l decl = - match decl, l with - | NamedDecl.LocalAssum (i,t), [] -> - [CompactedDecl.LocalAssum ([i],t)] - | NamedDecl.LocalDef (i,c,t), [] -> - [CompactedDecl.LocalDef ([i],c,t)] - | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> - if EConstr.eq_constr sigma t1 t2 - then CompactedDecl.LocalAssum (i1::li, t2) :: q - else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q - | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> - if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2 - then CompactedDecl.LocalDef (i1::li, c2, t2) :: q - else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q - | NamedDecl.LocalAssum (i,t), q -> - CompactedDecl.LocalAssum ([i],t) :: q - | NamedDecl.LocalDef (i,c,t), q -> - CompactedDecl.LocalDef ([i],c,t) :: q - in - sign |> Context.Named.fold_inside compact ~init:[] |> List.rev - let clear_named_body id env = let open NamedDecl in let aux _ status = function diff --git a/engine/termops.mli b/engine/termops.mli index e6badbac1940..625c3bb8115b 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -194,7 +194,6 @@ val fold_named_context_both_sides : ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> Constr.named_context -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Evd.evar_map -> EConstr.named_context -> EConstr.compacted_context val clear_named_body : Id.t -> env -> env diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml index 726b1a6f1e76..6f9aeb94b3ca 100644 --- a/ide/rocqide/idetop.ml +++ b/ide/rocqide/idetop.ml @@ -207,7 +207,7 @@ let process_goal short sigma g = if short then [] else let hyps = List.rev_map process_hyp - (Termops.compact_named_context sigma (EConstr.named_context env)) + (Ppconstr.compact_named_context sigma (EConstr.named_context env)) in hyps in diff --git a/kernel/constr.ml b/kernel/constr.ml index a05c35c581e6..e7051c6e4af6 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1383,10 +1383,8 @@ let hcons = HCons.hcons type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt -type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt type rel_context = rel_declaration list type named_context = named_declaration list -type compacted_context = compacted_declaration list (** Minimalistic constr printer, typically for debugging *) diff --git a/kernel/constr.mli b/kernel/constr.mli index c578e1d29798..edb0d9fe3cc8 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -430,10 +430,8 @@ val eq_constr_nounivs : constr -> constr -> bool type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt type named_declaration = (constr, types, Sorts.relevance) Context.Named.Declaration.pt -type compacted_declaration = (constr, types, Sorts.relevance) Context.Compacted.Declaration.pt type rel_context = rel_declaration list type named_context = named_declaration list -type compacted_context = compacted_declaration list (** {6 Relocation and substitution } *) diff --git a/kernel/context.ml b/kernel/context.ml index dbcdd89eb593..a0d9f84432eb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -569,32 +569,3 @@ struct let instance mk l = Array.of_list (instance_list mk l) end - -module Compacted = - struct - module Declaration = - struct - type ('constr, 'types, 'r) pt = - | LocalAssum of (Id.t,'r) pbinder_annot list * 'types - | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types - - let map_constr f = function - | LocalAssum (ids, ty) as decl -> - let ty' = f ty in - if ty == ty' then decl else LocalAssum (ids, ty') - | LocalDef (ids, c, ty) as decl -> - let ty' = f ty in - let c' = f c in - if c == c' && ty == ty' then decl else LocalDef (ids,c',ty') - - let of_named_decl = function - | Named.Declaration.LocalAssum (id,t) -> - LocalAssum ([id],t) - | Named.Declaration.LocalDef (id,v,t) -> - LocalDef ([id],v,t) - end - - type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list - - let fold f l ~init = List.fold_right f l init - end diff --git a/kernel/context.mli b/kernel/context.mli index e8d2e0e1d1b3..7d67681980ce 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -370,20 +370,3 @@ sig (** [instance_list] is like [instance] but returning a list. *) val instance_list : (Id.t -> 'v) -> ('c, 't, 'r) pt -> 'v list end - -module Compacted : -sig - module Declaration : - sig - type ('constr, 'types, 'r) pt = - | LocalAssum of (Id.t,'r) pbinder_annot list * 'types - | LocalDef of (Id.t,'r) pbinder_annot list * 'constr * 'types - - val map_constr : ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt - val of_named_decl : ('c, 't, 'r) Named.Declaration.pt -> ('c, 't, 'r) pt - end - - type ('constr, 'types, 'r) pt = ('constr, 'types, 'r) Declaration.pt list - - val fold : (('c, 't, 'r) Declaration.pt -> 'a -> 'a) -> ('c, 't, 'r) pt -> init:'a -> 'a -end diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index f792f9f7f252..ec7f4036788d 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -855,3 +855,42 @@ let pr_lconstr_pattern_expr ~flags env sigma c : Pp.t = !term_pr.pr_lconstr_patt let pr_cases_pattern_expr ~flags c : Pp.t = pr_patt ~flags (pr ~flags no_after ltop) no_after ltop c let pr_binders ~flags env sigma l : Pp.t = pr_undelimited_binders ~flags spc true (pr_expr ~flags env sigma no_after ltop) l + +module CompactedDecl = struct + type t = + | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types + | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types + + let of_named_decl = function + | Context.Named.Declaration.LocalAssum (id,t) -> + LocalAssum ([id],t) + | Context.Named.Declaration.LocalDef (id,v,t) -> + LocalDef ([id],v,t) + + let to_tuple = function + | LocalAssum (ids, t) -> ids, None, t + | LocalDef (ids, b, t) -> ids, Some b, t +end + +let compact_named_context sigma sign = + let module NamedDecl = Context.Named.Declaration in + let compact l decl = + match decl, l with + | NamedDecl.LocalAssum (i,t), [] -> + [CompactedDecl.LocalAssum ([i],t)] + | NamedDecl.LocalDef (i,c,t), [] -> + [CompactedDecl.LocalDef ([i],c,t)] + | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> + if EConstr.eq_constr sigma t1 t2 + then CompactedDecl.LocalAssum (i1::li, t2) :: q + else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q + | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> + if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2 + then CompactedDecl.LocalDef (i1::li, c2, t2) :: q + else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q + | NamedDecl.LocalAssum (i,t), q -> + CompactedDecl.LocalAssum ([i],t) :: q + | NamedDecl.LocalDef (i,c,t), q -> + CompactedDecl.LocalDef ([i],c,t) :: q + in + sign |> Context.Named.fold_inside compact ~init:[] |> List.rev diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index c1921f57fa3f..64bfedd59091 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -96,3 +96,17 @@ val modular_constr_pr : flags:flags -> ((unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t) -> (unit->Pp.t) -> int option -> entry_relative_level -> constr_expr -> Pp.t + +module CompactedDecl : sig + type t = + | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types + | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types + + val of_named_decl : EConstr.named_declaration -> t + + val to_tuple : t -> + Id.t EConstr.binder_annot list * + EConstr.constr option * + EConstr.types +end +val compact_named_context : Evd.evar_map -> EConstr.named_context -> CompactedDecl.t list diff --git a/printing/printer.ml b/printing/printer.ml index 4aa208ab0a5b..4c07453dd69e 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,7 +22,7 @@ open Declarations module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration -module CompactedDecl = Context.Compacted.Declaration +module CompactedDecl = Ppconstr.CompactedDecl (* This is set on by proofgeneral proof-tree mode. But may be used for other purposes *) @@ -363,33 +363,28 @@ let get_compact_context,set_compact_context = let compact_context = ref false in (fun () -> !compact_context),(fun b -> compact_context := b) -let pr_compacted_decl ?flags env sigma decl = +let pr_ecompacted_decl ?flags env sigma decl = let ids, pbody, typ = match decl with | CompactedDecl.LocalAssum (ids, typ) -> ids, None, typ | CompactedDecl.LocalDef (ids,c,typ) -> (* Force evaluation *) - let pb = pr_lconstr_env ?flags ~inctx:true env sigma c in - let pb = if isCast c then surround pb else pb in + let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in + let pb = if EConstr.isCast sigma c then surround pb else pb in ids, Some pb, typ in let pids = hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in - let pt = pr_ltype_env ?flags env sigma typ in + let pt = pr_letype_env ?flags env sigma typ in match pbody with | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt) | Some pbody -> hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt) -let pr_ecompacted_decl ?flags env sigma (decl:EConstr.compacted_declaration) = - let Refl = EConstr.Unsafe.eq in - pr_compacted_decl ?flags env sigma decl - -let pr_named_decl ?flags env sigma decl = - decl |> CompactedDecl.of_named_decl |> pr_compacted_decl ?flags env sigma +let pr_enamed_decl ?flags env sigma decl = + decl |> CompactedDecl.of_named_decl |> pr_ecompacted_decl ?flags env sigma -let pr_enamed_decl ?flags env sigma (decl:EConstr.named_declaration) = - let Refl = EConstr.Unsafe.eq in - pr_named_decl ?flags env sigma decl +let pr_named_decl ?flags env sigma (decl:Constr.named_declaration) = + pr_enamed_decl ?flags env sigma (EConstr.of_named_decl decl) let pr_rel_decl ?flags env sigma decl = let na = RelDecl.get_name decl in @@ -441,11 +436,11 @@ let pr_rel_context_of ?flags env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited ?flags env sigma = let sign_env = - Context.Compacted.fold + List.fold_right (fun d pps -> let pidt = pr_ecompacted_decl ?flags env sigma d in (pps ++ fnl () ++ pidt)) - (Termops.compact_named_context sigma (EConstr.named_context env)) ~init:(mt ()) + (compact_named_context sigma (EConstr.named_context env)) (mt ()) in let db_env = fold_rel_context @@ -496,7 +491,7 @@ and bld_sign_env_id ?flags env sigma ctxt pps is_start = spaces between simple hyps, and newline otherwise *) let pr_context_limit_compact ?n ?flags env sigma = let ctxt = EConstr.named_context env in - let ctxt = Termops.compact_named_context sigma ctxt in + let ctxt = compact_named_context sigma ctxt in let lgth = List.length ctxt in let n_capped = match n with diff --git a/printing/printer.mli b/printing/printer.mli index 2dbcf1a553d2..043932c33f0d 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -192,15 +192,13 @@ val pr_ne_context_of : Pp.t -> ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t val pr_named_decl : ?flags:PrintingFlags.t -> env -> evar_map -> Constr.named_declaration -> Pp.t -val pr_compacted_decl : ?flags:PrintingFlags.t -> - env -> evar_map -> Constr.compacted_declaration -> Pp.t val pr_rel_decl : ?flags:PrintingFlags.t -> env -> evar_map -> Constr.rel_declaration -> Pp.t val pr_enamed_decl : ?flags:PrintingFlags.t -> env -> evar_map -> EConstr.named_declaration -> Pp.t val pr_ecompacted_decl : ?flags:PrintingFlags.t -> - env -> evar_map -> EConstr.compacted_declaration -> Pp.t + env -> evar_map -> Ppconstr.CompactedDecl.t -> Pp.t val pr_erel_decl : ?flags:PrintingFlags.t -> env -> evar_map -> EConstr.rel_declaration -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 54f84dd6357a..33887bb8af5f 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -233,13 +233,6 @@ type goal = { ty: EConstr.t; env : Environ.env; sigma : Evd.evar_map; } (* XXX: Port to proofview, one day. *) (* open Proofview *) -module CDC = Context.Compacted.Declaration - -let to_tuple : EConstr.compacted_declaration -> (Names.Id.t EConstr.binder_annot list * 'pc option * 'pc) = - let open CDC in function - | LocalAssum(idl, tm) -> (idl, None, tm) - | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm) - let make_goal env sigma g = let evi = Evd.find_undefined sigma g in let env = Evd.evar_filtered_env env evi in @@ -297,7 +290,7 @@ let goal_info ~flags goal = let map = ref CString.Map.empty in let line_idents = ref [] in let build_hyp_info env sigma hyp = - let (names, body, ty) = to_tuple hyp in + let (names, body, ty) = Ppconstr.CompactedDecl.to_tuple hyp in let open Pp in let idents = List.map (fun x -> Names.Id.to_string x.Context.binder_name) names in @@ -318,7 +311,7 @@ let goal_info ~flags goal = try let { ty=ty; env=env; sigma } = goal in (* compaction is usually desired [eg for better display] *) - let hyps = Termops.compact_named_context sigma (EConstr.named_context env) in + let hyps = Ppconstr.compact_named_context sigma (EConstr.named_context env) in let () = List.iter (build_hyp_info env sigma) (List.rev hyps) in let concl_pp = pp_of_type ~flags env sigma ty in ( List.rev !line_idents, !map, concl_pp ) From ff75bf4db438595a5223b58a7bd5b4d22cadbead Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 19 May 2026 17:51:43 +0200 Subject: [PATCH 10/17] Debug flag for variable status --- dev/top_printers.ml | 2 +- .../proof-engine/vernacular-commands.rst | 6 ++ engine/eConstr.ml | 9 ++- engine/eConstr.mli | 7 ++- ide/rocqide/idetop.ml | 2 +- kernel/environ.ml | 22 ++++--- kernel/environ.mli | 9 ++- printing/ppconstr.ml | 42 +++++++------ printing/ppconstr.mli | 9 +-- printing/printer.ml | 59 +++++++++++-------- printing/printer.mli | 8 +-- printing/proof_diffs.ml | 2 +- test-suite/output/SecVar.out | 18 ++++++ test-suite/output/SecVar.v | 15 +++++ vernac/vernacentries.ml | 8 --- 15 files changed, 143 insertions(+), 75 deletions(-) create mode 100644 test-suite/output/SecVar.out create mode 100644 test-suite/output/SecVar.v diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e4a2c7717b12..d0a4a803dd77 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -318,7 +318,7 @@ let ppelim_constraints cstrs = pp (Sorts.ElimConstraints.pr qprinter cstrs) let ppnamedcontextval e = let env = Global.env () in let sigma = Evd.from_env env in - pp (pr_named_context env sigma (named_context_of_val e)) + pp (pr_named_context_of (Environ.reset_with_named_context e env) sigma) let ppaucontext auctx = let {quals = qnas; univs = unas} = AbstractContext.names auctx in diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 762d248d77fe..7b8bfd7f96fb 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1089,6 +1089,12 @@ Controlling display after each tactic. The information is used by the Prooftree tool in Proof General. (https://askra.de/software/prooftree) +.. flag:: Printing Variables Status + + This debug :term:`flag` prints whether each variable in the context + is a section variable or an hypothesis local to the current proof. + It is off by default. + .. extracted from Gallina extensions chapter .. _printing_constructions_full: diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 5f73db590b59..52f99c726532 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -1259,8 +1259,15 @@ let match_named_context_val : match unsafe_eq, unsafe_relevance_eq with | Refl, Refl -> match_named_context_val +let fold_named_context_val : + (named_context_val -> var_status -> named_declaration -> 'a -> 'a) -> + named_context_val -> init:'a -> 'a = + let Refl, Refl = unsafe_eq, unsafe_relevance_eq in + Environ.fold_named_context_val + let fold_named_context : - (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a = + (env -> var_status -> named_declaration -> 'a -> 'a) -> + env -> init:'a -> 'a = let Refl, Refl = unsafe_eq, unsafe_relevance_eq in Environ.fold_named_context diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 6d2cab493c23..7ee9a48ce89f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -433,8 +433,13 @@ val val_of_named_context : (var_status * named_declaration) list -> named_contex val named_context_of_val : named_context_val -> named_context val named_context_of_val_with_status : named_context_val -> (var_status * named_declaration) list +val fold_named_context_val : + (named_context_val -> var_status -> named_declaration -> 'a -> 'a) -> + named_context_val -> init:'a -> 'a + val fold_named_context : - (env -> var_status -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> var_status -> named_declaration -> 'a -> 'a) -> + env -> init:'a -> 'a val lookup_rel : int -> env -> rel_declaration val lookup_named : variable -> env -> named_declaration diff --git a/ide/rocqide/idetop.ml b/ide/rocqide/idetop.ml index 6f9aeb94b3ca..7afdb18ea3d9 100644 --- a/ide/rocqide/idetop.ml +++ b/ide/rocqide/idetop.ml @@ -207,7 +207,7 @@ let process_goal short sigma g = if short then [] else let hyps = List.rev_map process_hyp - (Ppconstr.compact_named_context sigma (EConstr.named_context env)) + (Ppconstr.compact_named_context sigma (Environ.named_context_val env)) in hyps in diff --git a/kernel/environ.ml b/kernel/environ.ml index 850bfe73e9e7..3a695cd15f67 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -191,6 +191,11 @@ let set_rel_context_val v env = (* Named context *) type var_status = SecVar | ProofVar +let var_status_eq a b = match a, b with + | SecVar, SecVar -> true + | ProofVar, ProofVar -> true + | (SecVar | ProofVar), _ -> false + let push_named_context_val status d ctxt = let id = NamedDecl.get_id d in (* assert (not (Id.Map.mem id ctxt.env_named_map)); *) @@ -519,15 +524,18 @@ let pop_rel_context n env = env_rel_context = skip n ctxt; env_nb_rel = env.env_nb_rel - n } -let fold_named_context f env ~init = - let rec fold_right env = - match match_named_context_val env.env_named_context with +let fold_named_context_val f sign ~init = + let rec fold_right sign = + match match_named_context_val sign with | None -> init | Some (status, d, rem) -> - let env = - reset_with_named_context rem env in - f env status d (fold_right env) - in fold_right env + f rem status d (fold_right rem) + in fold_right sign + +let fold_named_context f env ~init = + fold_named_context_val (fun sign status d acc -> + f (reset_with_named_context sign env) status d acc) + (named_context_val env) ~init let fold_named_context_reverse f ~init env = Context.Named.fold_inside f ~init:init (named_context env) diff --git a/kernel/environ.mli b/kernel/environ.mli index 477652dc15f5..3eff5eabcb78 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -113,6 +113,8 @@ val fold_rel_context : type var_status = SecVar | ProofVar +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 @@ -150,8 +152,13 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) +val fold_named_context_val : + (named_context_val -> var_status -> Constr.named_declaration -> 'a -> 'a) -> + named_context_val -> init:'a -> 'a + val fold_named_context : - (env -> var_status -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> var_status -> Constr.named_declaration -> 'a -> 'a) -> + env -> init:'a -> 'a val match_named_context_val : named_context_val -> (var_status * named_declaration * named_context_val) option diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index ec7f4036788d..f286f29b82af 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -858,39 +858,43 @@ let pr_binders ~flags env sigma l : Pp.t = pr_undelimited_binders ~flags spc tru module CompactedDecl = struct type t = - | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types - | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types + | LocalAssum of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.types + | LocalDef of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.constr * EConstr.types - let of_named_decl = function + let of_named_decl status = function | Context.Named.Declaration.LocalAssum (id,t) -> - LocalAssum ([id],t) + LocalAssum ([status,id], t) | Context.Named.Declaration.LocalDef (id,v,t) -> - LocalDef ([id],v,t) + LocalDef ([status,id], v, t) let to_tuple = function - | LocalAssum (ids, t) -> ids, None, t - | LocalDef (ids, b, t) -> ids, Some b, t + | LocalAssum (ids, t) -> List.map snd ids, None, t + | LocalDef (ids, b, t) -> List.map snd ids, Some b, t end let compact_named_context sigma sign = let module NamedDecl = Context.Named.Declaration in - let compact l decl = + let compact l status decl = match decl, l with | NamedDecl.LocalAssum (i,t), [] -> - [CompactedDecl.LocalAssum ([i],t)] + [CompactedDecl.LocalAssum ([Some status,i],t)] | NamedDecl.LocalDef (i,c,t), [] -> - [CompactedDecl.LocalDef ([i],c,t)] + [CompactedDecl.LocalDef ([Some status,i],c,t)] | NamedDecl.LocalAssum (i1,t1), CompactedDecl.LocalAssum (li,t2) :: q -> - if EConstr.eq_constr sigma t1 t2 - then CompactedDecl.LocalAssum (i1::li, t2) :: q - else CompactedDecl.LocalAssum ([i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q + if EConstr.eq_constr sigma t1 t2 + then CompactedDecl.LocalAssum ((Some status, i1)::li, t2) :: q + else CompactedDecl.LocalAssum ([Some status, i1],t1) :: CompactedDecl.LocalAssum (li,t2) :: q | NamedDecl.LocalDef (i1,c1,t1), CompactedDecl.LocalDef (li,c2,t2) :: q -> - if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2 - then CompactedDecl.LocalDef (i1::li, c2, t2) :: q - else CompactedDecl.LocalDef ([i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q + if EConstr.eq_constr sigma c1 c2 && EConstr.eq_constr sigma t1 t2 + then CompactedDecl.LocalDef ((Some status, i1)::li, c2, t2) :: q + else CompactedDecl.LocalDef ([Some status, i1],c1,t1) :: CompactedDecl.LocalDef (li,c2,t2) :: q | NamedDecl.LocalAssum (i,t), q -> - CompactedDecl.LocalAssum ([i],t) :: q + CompactedDecl.LocalAssum ([Some status,i],t) :: q | NamedDecl.LocalDef (i,c,t), q -> - CompactedDecl.LocalDef ([i],c,t) :: q + CompactedDecl.LocalDef ([Some status,i],c,t) :: q in - sign |> Context.Named.fold_inside compact ~init:[] |> List.rev + let ctx = EConstr.fold_named_context_val (fun _ status d acc -> compact acc status d) sign ~init:[] in + List.map (function + | CompactedDecl.LocalAssum (ids, t) -> CompactedDecl.LocalAssum (List.rev ids, t) + | CompactedDecl.LocalDef (ids, a, b) -> CompactedDecl.LocalDef (List.rev ids, a, b)) + ctx diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 64bfedd59091..7735b7ff1856 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -99,14 +99,15 @@ val modular_constr_pr : module CompactedDecl : sig type t = - | LocalAssum of Id.t EConstr.binder_annot list * EConstr.types - | LocalDef of Id.t EConstr.binder_annot list * EConstr.constr * EConstr.types + | LocalAssum of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.types + | LocalDef of (Environ.var_status option * Id.t EConstr.binder_annot) list * EConstr.constr * EConstr.types - val of_named_decl : EConstr.named_declaration -> t + val of_named_decl : Environ.var_status option -> EConstr.named_declaration -> t val to_tuple : t -> Id.t EConstr.binder_annot list * EConstr.constr option * EConstr.types end -val compact_named_context : Evd.evar_map -> EConstr.named_context -> CompactedDecl.t list + +val compact_named_context : Evd.evar_map -> Environ.named_context_val -> CompactedDecl.t list diff --git a/printing/printer.ml b/printing/printer.ml index 4c07453dd69e..1021090fa7c4 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -359,32 +359,42 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (* Flag for compact display of goals *) -let get_compact_context,set_compact_context = - let compact_context = ref false in - (fun () -> !compact_context),(fun b -> compact_context := b) +let { Goptions.get = get_compact_context } = + Goptions.declare_bool_option_and_ref ~key:["Printing";"Compact";"Contexts"] ~value:false () + +let { Goptions.get = print_var_status } = + Goptions.declare_bool_option_and_ref ~key:["Printing";"Variables";"Status"] ~value:false () let pr_ecompacted_decl ?flags env sigma decl = let ids, pbody, typ = match decl with | CompactedDecl.LocalAssum (ids, typ) -> - ids, None, typ - | CompactedDecl.LocalDef (ids,c,typ) -> - (* Force evaluation *) - let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in - let pb = if EConstr.isCast sigma c then surround pb else pb in - ids, Some pb, typ in + ids, None, typ + | CompactedDecl.LocalDef (ids, c, typ) -> + (* Force evaluation *) + let pb = pr_leconstr_env ?flags ~inctx:true env sigma c in + let pb = if EConstr.isCast sigma c then surround pb else pb in + ids, Some pb, typ in + let pp_status status = + if print_var_status() then + match status with + | None -> mt() + | Some SecVar -> spc() ++ pr_in_comment (str "section variable") + | Some ProofVar -> spc() ++ pr_in_comment (str "hypothesis") + else mt() + in let pids = - hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in + hov 0 (prlist_with_sep pr_comma (fun (status, id) -> pr_id id.binder_name ++ pp_status status) ids) in let pt = pr_letype_env ?flags env sigma typ in match pbody with | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt) | Some pbody -> - hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt) + hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt) -let pr_enamed_decl ?flags env sigma decl = - decl |> CompactedDecl.of_named_decl |> pr_ecompacted_decl ?flags env sigma +let pr_enamed_decl ?flags env sigma status decl = + decl |> CompactedDecl.of_named_decl status |> pr_ecompacted_decl ?flags env sigma -let pr_named_decl ?flags env sigma (decl:Constr.named_declaration) = - pr_enamed_decl ?flags env sigma (EConstr.of_named_decl decl) +let pr_named_decl ?flags env sigma status (decl:Constr.named_declaration) = + pr_enamed_decl ?flags env sigma status (EConstr.of_named_decl decl) let pr_rel_decl ?flags env sigma decl = let na = RelDecl.get_name decl in @@ -412,19 +422,18 @@ let pr_erel_decl ?flags env sigma (decl:EConstr.rel_declaration) = * It's printed out from outermost to innermost, so it's readable. *) (* Prints a signature, all declarations on the same line if possible *) + +let pr_named_context ?flags env sigma ctx = + hv 0 (prlist_with_sep (fun () -> ws 2) (fun d -> pr_named_decl ?flags env sigma None d) ctx) + let pr_named_context_of ?flags env sigma = - let make_decl_list env _status d pps = pr_named_decl ?flags env sigma d :: pps in + let make_decl_list env status d pps = pr_named_decl ?flags env sigma (Some status) d :: pps in let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) let pr_var_list_decl ?flags env sigma decl = hov 0 (pr_ecompacted_decl ?flags env sigma decl) -let pr_named_context ?flags env sigma ne_context = - hv 0 (Context.Named.fold_outside - (fun d pps -> pps ++ ws 2 ++ pr_named_decl ?flags env sigma d) - ne_context ~init:(mt ())) - let pr_rel_context ?(flags=current_combined()) env sigma rel_context = let ppflags = Ppconstr.of_printing_flags flags in let rel_context = EConstr.of_rel_context rel_context in @@ -440,7 +449,7 @@ let pr_context_unlimited ?flags env sigma = (fun d pps -> let pidt = pr_ecompacted_decl ?flags env sigma d in (pps ++ fnl () ++ pidt)) - (compact_named_context sigma (EConstr.named_context env)) (mt ()) + (compact_named_context sigma (Environ.named_context_val env)) (mt ()) in let db_env = fold_rel_context @@ -469,7 +478,7 @@ let should_compact env sigma typ = let rec bld_sign_env ?flags env sigma ctxt pps = match ctxt with | [] -> pps - | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ -> + | CompactedDecl.LocalAssum (_,typ)::ctxt' when should_compact env sigma typ -> let pps',ctxt' = bld_sign_env_id ?flags env sigma ctxt (mt ()) true in (* putting simple hyps in a more horizontal flavor *) bld_sign_env ?flags env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps') @@ -480,7 +489,7 @@ let rec bld_sign_env ?flags env sigma ctxt pps = and bld_sign_env_id ?flags env sigma ctxt pps is_start = match ctxt with | [] -> pps,ctxt - | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> + | CompactedDecl.LocalAssum(_,typ) as d :: ctxt' when should_compact env sigma typ -> let pidt = pr_var_list_decl ?flags env sigma d in let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in bld_sign_env_id ?flags env sigma ctxt' pps' false @@ -490,7 +499,7 @@ and bld_sign_env_id ?flags env sigma ctxt pps is_start = (* compact printing an env (variables and de Bruijn). Separator: three spaces between simple hyps, and newline otherwise *) let pr_context_limit_compact ?n ?flags env sigma = - let ctxt = EConstr.named_context env in + let ctxt = Environ.named_context_val env in let ctxt = compact_named_context sigma ctxt in let lgth = List.length ctxt in let n_capped = diff --git a/printing/printer.mli b/printing/printer.mli index 043932c33f0d..7413d617f289 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -183,20 +183,16 @@ val pr_notation_interpretation_env : env -> evar_map -> glob_constr -> Pp.t (** Contexts *) -(** Display compact contexts of goals (simple hyps on the same line) *) -val set_compact_context : bool -> unit -val get_compact_context : unit -> bool - val pr_context_unlimited : ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t val pr_ne_context_of : Pp.t -> ?flags:PrintingFlags.t -> env -> evar_map -> Pp.t val pr_named_decl : ?flags:PrintingFlags.t -> - env -> evar_map -> Constr.named_declaration -> Pp.t + env -> evar_map -> var_status option -> Constr.named_declaration -> Pp.t val pr_rel_decl : ?flags:PrintingFlags.t -> env -> evar_map -> Constr.rel_declaration -> Pp.t val pr_enamed_decl : ?flags:PrintingFlags.t -> - env -> evar_map -> EConstr.named_declaration -> Pp.t + env -> evar_map -> var_status option -> EConstr.named_declaration -> Pp.t val pr_ecompacted_decl : ?flags:PrintingFlags.t -> env -> evar_map -> Ppconstr.CompactedDecl.t -> Pp.t val pr_erel_decl : ?flags:PrintingFlags.t -> diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 33887bb8af5f..12eec5366745 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -311,7 +311,7 @@ let goal_info ~flags goal = try let { ty=ty; env=env; sigma } = goal in (* compaction is usually desired [eg for better display] *) - let hyps = Ppconstr.compact_named_context sigma (EConstr.named_context env) in + let hyps = Ppconstr.compact_named_context sigma (Environ.named_context_val env) in let () = List.iter (build_hyp_info env sigma) (List.rev hyps) in let concl_pp = pp_of_type ~flags env sigma ty in ( List.rev !line_idents, !map, concl_pp ) diff --git a/test-suite/output/SecVar.out b/test-suite/output/SecVar.out new file mode 100644 index 000000000000..6f32683e6776 --- /dev/null +++ b/test-suite/output/SecVar.out @@ -0,0 +1,18 @@ +1 goal + + a (* section variable *), b (* section variable *) : nat + H (* section variable *) : a = b + ============================ + True +1 goal + + a (* section variable *), b (* section variable *) : nat + H (* hypothesis *) : b = a + ============================ + True +1 goal + + a (* section variable *), y (* hypothesis *) : nat + H (* hypothesis *) : y = a + ============================ + True diff --git a/test-suite/output/SecVar.v b/test-suite/output/SecVar.v new file mode 100644 index 000000000000..82116643fa3a --- /dev/null +++ b/test-suite/output/SecVar.v @@ -0,0 +1,15 @@ +Section S. + Variables a b : nat. + Variable H : a = b. + + Set Printing Variables Status. + + Goal True. + Proof. + Show. + apply eq_sym in H. + Show. + rename b into y. + Show. + Abort. +End S. diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 86adb56b5020..5e9b897fdea7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1943,14 +1943,6 @@ let () = optread = (fun () -> (Global.typing_flags ()).Declarations.unfold_dep_heuristic); optwrite = Global.set_unfold_dep_heuristic } -let () = - declare_bool_option - { optstage = Summary.Stage.Interp; - optdepr = None; - optkey = ["Printing";"Compact";"Contexts"]; - optread = (fun () -> Printer.get_compact_context()); - optwrite = (fun b -> Printer.set_compact_context b) } - let () = declare_int_option { optstage = Summary.Stage.Interp; From f977070a65022de8dacda2fb7c89314a211f0680 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 20 May 2026 16:57:05 +0200 Subject: [PATCH 11/17] uncomment assert in environ when this invariant is broken secvar checking produces another assert failure later --- kernel/environ.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index 3a695cd15f67..f171ec2e77b4 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -198,7 +198,7 @@ let var_status_eq a b = match a, b with let push_named_context_val status d ctxt = let id = NamedDecl.get_id d in - (* assert (not (Id.Map.mem id ctxt.env_named_map)); *) + assert (not (Id.Map.mem id ctxt.env_named_map)); let secvars = match status with | ProofVar -> ctxt.env_named_secvars | SecVar -> Id.Set.add id ctxt.env_named_secvars From 3452ac2a82aeaad541a3141f7e8d016726d8b621 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 21 May 2026 17:41:49 +0200 Subject: [PATCH 12/17] bench auto overlays for metarocq --- dev/bench/bench.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/dev/bench/bench.sh b/dev/bench/bench.sh index 47be3fc4a216..37202ededc15 100755 --- a/dev/bench/bench.sh +++ b/dev/bench/bench.sh @@ -98,6 +98,7 @@ export COQ_LOG_DIR=$log_dir declare -A auto_overlay_map auto_overlay_map[elpi]="rocq-elpi" auto_overlay_map[equations]="rocq-equations" +auto_overlay_map[metarocq]="rocq-metarocq-utils rocq-metarocq-common rocq-metarocq-template rocq-metarocq-pcuic rocq-metarocq-safechecker rocq-metarocq-erasure rocq-metarocq-translations" if [ "$auto_overlays" ]; then CI_PULL_REQUEST="${CI_COMMIT_REF_NAME#pr-}" From 395a8d80987125f03bd244fa1643b71af4555bd5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 27 May 2026 14:28:20 +0200 Subject: [PATCH 13/17] add is_section_var tactic Close #21104 --- doc/sphinx/proof-engine/ltac.rst | 8 ++++++++ doc/tools/docgram/fullGrammar | 1 + doc/tools/docgram/orderedGrammar | 1 + plugins/ltac/extratactics.mlg | 4 ++++ plugins/ltac/internals.ml | 14 ++++++++++++++ plugins/ltac/internals.mli | 1 + 6 files changed, 29 insertions(+) diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index f88e0ad5775f..7ea13b8843a0 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1706,6 +1706,14 @@ succeeds, and results in an error otherwise. .. exn:: Not a variable or hypothesis. :undocumented: +.. tacn:: is_section_var @one_term + + Succeeds if :n:`@one_term` is a section variable in + the current local context and fails otherwise. + + .. exn:: Not a section variable. + :undocumented: + .. tacn:: is_const @one_term Succeeds if :n:`@one_term` is a global constant that is neither a (co)inductive diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index 38c9d327a6f8..1e2a661598d2 100644 --- a/doc/tools/docgram/fullGrammar +++ b/doc/tools/docgram/fullGrammar @@ -1826,6 +1826,7 @@ simple_tactic: [ | "is_evar" constr | "has_evar" constr | "is_var" constr +| "is_section_var" constr | "is_fix" constr | "is_cofix" constr | "is_ind" constr diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d677407a4f1b..bf3fca66453f 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1498,6 +1498,7 @@ simple_tactic: [ | "is_evar" one_term | "has_evar" one_term | "is_var" one_term +| "is_section_var" one_term | "is_fix" one_term | "is_cofix" one_term | "is_ind" one_term diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index fc0cb6611fe0..30c7aff4d81b 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -505,6 +505,10 @@ TACTIC EXTEND is_hyp | [ "is_var" constr(x) ] -> { Internals.is_var x } END +TACTIC EXTEND is_secvar +| [ "is_section_var" constr(x) ] -> { Internals.is_section_var x } +END + TACTIC EXTEND is_fix | [ "is_fix" constr(x) ] -> { Internals.is_fix x } END diff --git a/plugins/ltac/internals.ml b/plugins/ltac/internals.ml index 7bf5ab378113..4efe423e653b 100644 --- a/plugins/ltac/internals.ml +++ b/plugins/ltac/internals.ml @@ -126,6 +126,20 @@ let is_var x = | Var _ -> Proofview.tclUNIT () | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis") +let is_section_var x = + (* we can enter_one because a constr argument is focusing *) + Proofview.Goal.enter_one ~__LOC__ begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + match EConstr.kind sigma x with + | Var id -> + (* check:false because we don't want to anomaly here if the user + sneaks in some unbound variable *) + if Termops.is_section_variable' ~check:false env id then Proofview.tclUNIT () + else Tacticals.tclFAIL (Pp.str "Not a section variable.") + | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis.") + end + let is_fix x = Proofview.tclEVARMAP >>= fun sigma -> match EConstr.kind sigma x with diff --git a/plugins/ltac/internals.mli b/plugins/ltac/internals.mli index 027debcc3ac8..3d9090326c71 100644 --- a/plugins/ltac/internals.mli +++ b/plugins/ltac/internals.mli @@ -44,6 +44,7 @@ val refine_tac : Tacinterp.interp_sign -> simple:bool -> with_classes:bool -> val has_evar : EConstr.t -> unit tactic val is_evar : EConstr.t -> unit tactic val is_var : EConstr.t -> unit tactic +val is_section_var : EConstr.t -> unit tactic val is_fix : EConstr.t -> unit tactic val is_cofix : EConstr.t -> unit tactic val is_ind : EConstr.t -> unit tactic From 9fd9307754d3479d241be379104538cacfcd0ae0 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 20 May 2026 15:41:36 +0200 Subject: [PATCH 14/17] overlay --- .../21987-SkySkimmer-context-secvar.sh | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) create mode 100644 dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh diff --git a/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh new file mode 100644 index 000000000000..011d5f234b70 --- /dev/null +++ b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh @@ -0,0 +1,34 @@ +overlay equations https://github.com/SkySkimmer/equations context-secvar 21987 + +overlay elpi https://github.com/SkySkimmer/coq-elpi context-secvar 21987 + +overlay mathcomp https://github.com/SkySkimmer/math-comp context-secvar 21987 + +overlay tlc https://github.com/SkySkimmer/tlc context-secvar 21987 + +overlay kami https://github.com/SkySkimmer/kami context-secvar 21987 +# Make PRs against https://github.com/mit-plv/kami base branch rv32i + +overlay metarocq https://github.com/SkySkimmer/metarocq context-secvar 21987 + +overlay bedrock2 https://github.com/SkySkimmer/bedrock2 context-secvar 21987 +# Make PRs against https://github.com/mit-plv/bedrock2 base branch master + +overlay coqutil https://github.com/SkySkimmer/coqutil context-secvar 21987 +# Make PRs against https://github.com/mit-plv/coqutil base branch master + +overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto context-secvar 21987 + +overlay ceres https://github.com/SkySkimmer/coq-ceres context-secvar 21987 + +overlay unicoq https://github.com/SkySkimmer/unicoq context-secvar 21987 + +overlay mtac2 https://github.com/SkySkimmer/Mtac2 context-secvar 21987 + +overlay rocq_lsp https://github.com/SkySkimmer/rocq-lsp context-secvar 21987 + +overlay tactician https://github.com/SkySkimmer/coq-tactician context-secvar 21987 + +overlay vsrocq https://github.com/SkySkimmer/vsrocq context-secvar 21987 + +overlay waterproof https://github.com/SkySkimmer/coq-waterproof context-secvar 21987 From db319703a0f9340952ddc82defed693efcb3f088 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Wed, 27 May 2026 16:25:35 +0200 Subject: [PATCH 15/17] weaken assert in push_named --- kernel/environ.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/kernel/environ.ml b/kernel/environ.ml index f171ec2e77b4..7f5295a5e76a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -198,7 +198,9 @@ let var_status_eq a b = match a, b with let push_named_context_val status d ctxt = let id = NamedDecl.get_id d in - assert (not (Id.Map.mem id ctxt.env_named_map)); + (* we would like the stronger assert but it breaks in bug_4095 *) + (* assert (not (Id.Map.mem id ctxt.env_named_map)); *) + assert (not (Id.Set.mem id ctxt.env_named_secvars)); let secvars = match status with | ProofVar -> ctxt.env_named_secvars | SecVar -> Id.Set.add id ctxt.env_named_secvars From 66dc56d25fc99ce0de927e986b4fe300946a1e9d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 28 May 2026 14:39:11 +0200 Subject: [PATCH 16/17] disable some not needed overlays --- dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh index 011d5f234b70..d0bb28df466e 100644 --- a/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh +++ b/dev/ci/user-overlays/21987-SkySkimmer-context-secvar.sh @@ -2,9 +2,9 @@ overlay equations https://github.com/SkySkimmer/equations context-secvar 21987 overlay elpi https://github.com/SkySkimmer/coq-elpi context-secvar 21987 -overlay mathcomp https://github.com/SkySkimmer/math-comp context-secvar 21987 +#overlay mathcomp https://github.com/SkySkimmer/math-comp context-secvar 21987 -overlay tlc https://github.com/SkySkimmer/tlc context-secvar 21987 +#overlay tlc https://github.com/SkySkimmer/tlc context-secvar 21987 overlay kami https://github.com/SkySkimmer/kami context-secvar 21987 # Make PRs against https://github.com/mit-plv/kami base branch rv32i @@ -19,7 +19,7 @@ overlay coqutil https://github.com/SkySkimmer/coqutil context-secvar 21987 overlay fiat_crypto https://github.com/SkySkimmer/fiat-crypto context-secvar 21987 -overlay ceres https://github.com/SkySkimmer/coq-ceres context-secvar 21987 +#overlay ceres https://github.com/SkySkimmer/coq-ceres context-secvar 21987 overlay unicoq https://github.com/SkySkimmer/unicoq context-secvar 21987 From 60156a00dddba384b5174fd10dff2282f532b30e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Mon, 1 Jun 2026 17:11:57 +0200 Subject: [PATCH 17/17] Rename is_section_variable' -> is_section_variable_env --- engine/evarutil.ml | 6 +++--- engine/termops.ml | 2 +- engine/termops.mli | 4 ++-- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/ltac/internals.ml | 2 +- tactics/equality.ml | 2 +- tactics/hints.ml | 2 +- tactics/induction.ml | 4 ++-- 8 files changed, 12 insertions(+), 12 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index e51486d69b81..7adf698fc061 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -571,7 +571,7 @@ let rec check_and_clear_in_constr env evdref err ids ~global c = try let nids = Id.Map.domain rids in let env = evar_filtered_env env evi in - let global = Id.Set.exists (is_section_variable' env) nids in + let global = Id.Set.exists (is_section_variable_env env) nids in let concl = evar_concl evi in check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids ~global concl with ClearDependencyError (rid,err,where) -> @@ -592,7 +592,7 @@ let clear_hyps_in_evi_main env sigma hyps terms ids = hypothesis does not depend on a element of ids, and erases ids in the contexts of the evars occurring in evi *) let evdref = ref sigma in - let global = Id.Set.exists (is_section_variable' env) ids in + let global = Id.Set.exists (is_section_variable_env env) ids in let terms = List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids ~global) terms in let nhyps = @@ -607,7 +607,7 @@ let clear_hyps_in_evi_main env sigma hyps terms ids = let check_and_clear_in_constr env evd err ids c = let evdref = ref evd in - let global = Id.Set.exists (is_section_variable' env) ids in + let global = Id.Set.exists (is_section_variable_env env) ids in let _ : EConstr.constr = check_and_clear_in_constr ~global env evdref err ids c diff --git a/engine/termops.ml b/engine/termops.ml index c9b8643fadd7..70659d9389da 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1011,7 +1011,7 @@ let is_section_variable_sign ?check sign id = | SecVar -> true | ProofVar -> false -let is_section_variable' ?check env id = +let is_section_variable_env ?check env id = is_section_variable_sign ?check (Environ.named_context_val env) id let is_template_polymorphic_ref env sigma f = diff --git a/engine/termops.mli b/engine/termops.mli index 625c3bb8115b..167713da5211 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -207,13 +207,13 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id. (** This tests if the ident is known in the given env, intended to be used with the global env. *) val is_section_variable : env -> Id.t -> bool -[@@deprecated "Use is_section_variable' on the local env instead of is_section_variable on the global env."] +[@@deprecated "Use is_section_variable_env on the local env instead of is_section_variable on the global env."] (** Check if the ident has [SecVar] status in this enviroment. By default [check=true] and produce anomaly if it is not bound. If [check=false] returns [false] if it is not bound. *) val is_section_variable_sign : ?check:bool -> Environ.named_context_val -> Id.t -> bool -val is_section_variable' : ?check:bool -> env -> Id.t -> bool +val is_section_variable_env : ?check:bool -> env -> Id.t -> bool val is_template_polymorphic_ref : env -> Evd.evar_map -> constr -> bool val is_template_polymorphic_ind : env -> Evd.evar_map -> constr -> bool diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 6eb38126f814..7238bc3eb7c3 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -800,7 +800,7 @@ let generalize_non_dep hyp = Id.List.mem hyp hyps || List.exists (Termops.occur_var_in_decl env sigma hyp) keep || Termops.occur_var env sigma hyp hyp_typ - || Termops.is_section_variable' env hyp + || Termops.is_section_variable_env env hyp (* should be dangerous *) then (clear, decl :: keep) else (hyp :: clear, keep)) diff --git a/plugins/ltac/internals.ml b/plugins/ltac/internals.ml index 4efe423e653b..53a8b4175fb1 100644 --- a/plugins/ltac/internals.ml +++ b/plugins/ltac/internals.ml @@ -135,7 +135,7 @@ let is_section_var x = | Var id -> (* check:false because we don't want to anomaly here if the user sneaks in some unbound variable *) - if Termops.is_section_variable' ~check:false env id then Proofview.tclUNIT () + if Termops.is_section_variable_env ~check:false env id then Proofview.tclUNIT () else Tacticals.tclFAIL (Pp.str "Not a section variable.") | _ -> Tacticals.tclFAIL (Pp.str "Not a variable or hypothesis.") end diff --git a/tactics/equality.ml b/tactics/equality.ml index e50536e57768..9292bed8a0a8 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1849,7 +1849,7 @@ let subst_one_var dep_proof_ok x = (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in - if is_section_variable' env x then + if is_section_variable_env env x then check_non_indirectly_dependent_section_variable gl x; subst_one dep_proof_ok x res end diff --git a/tactics/hints.ml b/tactics/hints.ml index 9d9bd3ff7869..698af4e61d68 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -898,7 +898,7 @@ let with_uid c = { obj = c; uid = fresh_key () } variable, [secvars_of_global _ (VarRef x)] should return the empty set *) let secvars_of_idset env s = Id.Set.fold (fun id p -> - if is_section_variable' env id then + if is_section_variable_env env id then Id.Pred.add id p else p) s Id.Pred.empty diff --git a/tactics/induction.ml b/tactics/induction.ml index a0ef78585cc2..191708085726 100644 --- a/tactics/induction.ml +++ b/tactics/induction.ml @@ -1397,7 +1397,7 @@ let induction_gen ~clear_flag ~isrec ~with_evars elim let cls = Option.default allHypsAndConcl cls in let t = typ_of env evd c in let is_arg_pure_hyp = - isVar evd c && not (is_section_variable' env (destVar evd c)) + isVar evd c && not (is_section_variable_env env (destVar evd c)) && lbind == NoBindings && not with_evars && Option.is_empty eqname && clear_flag == None && has_generic_occurrences_but_goal cls (destVar evd c) env evd ccl in @@ -1449,7 +1449,7 @@ let induction_gen_l isrec with_evars elim names lc = let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in match EConstr.kind sigma c with - | Var id when not (is_section_variable' env id) + | Var id when not (is_section_variable_env env id) && not with_evars -> let () = newlc:= id::!newlc in atomize_list l'