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

Author: SkySkimmer

engine/evarutil.ml

@@ -285,18 +285,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,31 +585,31 @@ 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 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
+      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
   (!evdref, nhyps, terms)
 
 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

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)
 
@@ -240,7 +228,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
@@ -249,10 +237,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
 

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,15 +397,15 @@ 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) =
   let id = match na with
     | 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

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 sign id =
+  match NamedDecl.get_status @@ Environ.lookup_named_ctxt id sign with
+  | exception Not_found -> assert false
+  | SecVar -> true
+  | ProofVar -> false
+
+let is_section_variable' env id = is_section_variable_sign (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

engine/termops.mli

@@ -206,8 +206,13 @@ 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, indented 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. [false] if it is not bound. *)
+val is_section_variable_sign : Environ.named_context_val -> Id.t -> bool
+val is_section_variable' : 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

kernel/context.ml

@@ -355,6 +355,10 @@ struct
 
     let get_status (LocalAssum (s,_,_) | LocalDef (s,_,_,_)) = s
 
+    let is_secvar d = match get_status d with
+      | SecVar -> true
+      | ProofVar -> false
+
     let get_annot = function
       | LocalAssum (_,na,_) | LocalDef (_,na,_,_) -> na
 

kernel/context.mli

@@ -235,6 +235,8 @@ sig
 
     val get_status : _ pt -> status
 
+    val is_secvar : _ pt -> bool
+
     val get_annot : (_,_,'r) pt -> (Id.t,'r) pbinder_annot
 
     (** Return the identifier bound by a given declaration. *)

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))

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'

plugins/ltac/leminv.ml

@@ -201,12 +201,11 @@ 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 d sign ->
         let d = EConstr.of_named_decl d in
-         if mem_named_context_val (NamedDecl.get_id d) global_named_context then sign
+         if NamedDecl.is_secvar d then sign
          else Context.Named.add d sign)
       invEnv ~init:Context.Named.empty
   end in