Generalize DeclareScheme to use GlobRef instead of inductive

thomas-lamiaux · thomas-lamiaux · commit 11efe8256bf8 · 2026-03-27T19:04:08.000+01:00
prevent registering scheme for section variables without the local attribute
diff --git a/dev/ci/user-overlays/21811-thomas-lamiaux-genScheme.sh b/dev/ci/user-overlays/21811-thomas-lamiaux-genScheme.sh
@@ -0,0 +1 @@
+overlay elpi https://github.com/thomas-lamiaux/coq-elpi genScheme 21811
diff --git a/doc/changelog/04-tactics/21811-genScheme-Changed.rst b/doc/changelog/04-tactics/21811-genScheme-Changed.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  Generalize DeclareScheme to be able to register schemes for any GlobRef,
+  and not just for inductive types
+  (`#21811 <https://github.com/rocq-prover/rocq/pull/21811>`_,
+  by Thomas Lamiaux).
diff --git a/tactics/allScheme.ml b/tactics/allScheme.ml
@@ -293,22 +293,22 @@ let warn_lookup_not_found =
     Raise a warning if none is found. *)
 let lookup_all ind ind_nested args_are_nested =
     let (_, (pred, _)) = partial_suffix args_are_nested in
-    match DeclareScheme.lookup_scheme_opt  pred ind_nested with
+    match DeclareScheme.lookup_scheme_opt pred (GlobRef.IndRef ind_nested) with
     | Some ref_pred ->
         Some (true, ref_pred)
     | None ->
         let (_, (pred, _)) = default_suffix in
-        match DeclareScheme.lookup_scheme_opt  pred ind_nested with
+        match DeclareScheme.lookup_scheme_opt pred (GlobRef.IndRef ind_nested) with
         | Some ref_pred -> Some (false, ref_pred)
         | None -> warn_lookup_not_found (pred, ind, ind_nested); None
 
 (** Lookup the [all] predicate, and its theorem *)
 let lookup_all_theorem_aux ind ind_nested =
   let (_, (pred, thm)) = default_suffix in
-  match DeclareScheme.lookup_scheme_opt pred ind_nested with
+  match DeclareScheme.lookup_scheme_opt pred (GlobRef.IndRef ind_nested) with
   | None -> warn_lookup_not_found (pred, ind, ind_nested); None
   | Some ref_pred ->
-      match DeclareScheme.lookup_scheme_opt thm ind_nested with
+      match DeclareScheme.lookup_scheme_opt thm (GlobRef.IndRef ind_nested) with
       | None -> warn_lookup_not_found (thm, ind, ind_nested); None
       | Some ref_thm -> Some (false, ref_pred, ref_thm)
 
@@ -318,10 +318,10 @@ let lookup_all_theorem_aux ind ind_nested =
     Raise a warning if none is found. *)
 let lookup_all_theorem ind ind_nested args_are_nested =
   let (_, (pred, thm)) = partial_suffix args_are_nested in
-  match DeclareScheme.lookup_scheme_opt pred ind_nested with
+  match DeclareScheme.lookup_scheme_opt pred (GlobRef.IndRef ind_nested) with
   | None -> lookup_all_theorem_aux ind ind_nested
   | Some ref_pred ->
-      match DeclareScheme.lookup_scheme_opt  thm ind_nested with
+      match DeclareScheme.lookup_scheme_opt thm (GlobRef.IndRef ind_nested) with
       | Some ref_thm ->
           Some (true, ref_pred, ref_thm)
       | None ->
diff --git a/tactics/declareScheme.ml b/tactics/declareScheme.ml
@@ -10,37 +10,45 @@
 
 open Names
 
-let scheme_map = Summary.ref Indmap_env.empty ~name:"Schemes"
+let scheme_map = Summary.ref GlobRef.Map_env.empty ~name:"Schemes"
 
-let cache_one_scheme kind (ind,const) =
-  scheme_map := Indmap_env.update ind (function
+let cache_one_scheme kind (gr,const) =
+  scheme_map := GlobRef.Map_env.update gr (function
       | None -> Some (CString.Map.singleton kind const)
       | Some map -> Some (CString.Map.add kind const map))
       !scheme_map
 
 let cache_scheme (kind,l) =
   cache_one_scheme kind l
 
-let subst_one_scheme subst (ind,const) =
-  (* Remark: const is a def: the result of substitution is a constant *)
-  (Mod_subst.subst_ind subst ind, Globnames.subst_global_reference subst const)
+let subst_one_scheme subst (gr,const) =
+  (Globnames.subst_global_reference subst gr, Globnames.subst_global_reference subst const)
 
 let subst_scheme (subst,(kind,l)) =
   (kind, subst_one_scheme subst l)
 
-let inScheme : Libobject.locality * (string * (inductive * GlobRef.t)) -> Libobject.obj =
+let inScheme : Libobject.locality * (string * (GlobRef.t * GlobRef.t)) -> Libobject.obj =
   let open Libobject in
   declare_object @@ object_with_locality "SCHEME"
     ~cache:cache_scheme
     ~subst:(Some subst_scheme)
     ~discharge:(fun x -> x)
 
-let declare_scheme local kind indcl =
-  Lib.add_leaf (inScheme (local,(kind,indcl)))
-
-let lookup_scheme kind ind = CString.Map.find kind (Indmap_env.find ind !scheme_map)
-
-let lookup_scheme_opt kind ind =
-  try Some (lookup_scheme kind ind) with Not_found -> None
+let declare_scheme local kind (gr, _ as grcl) =
+  let () = match local, gr with
+  | (Libobject.Export | Libobject.SuperGlobal), GlobRef.VarRef id ->
+    if Global.is_in_section gr then
+      CErrors.user_err
+        Pp.(str "Cannot register a non-local scheme for section variable "
+            ++ Names.Id.print id
+            ++ str "; use the #[local] attribute.")
+  | _, _ -> ()
+  in
+  Lib.add_leaf (inScheme (local,(kind,grcl)))
+
+let lookup_scheme kind gr = CString.Map.find kind (GlobRef.Map_env.find gr !scheme_map)
+
+let lookup_scheme_opt kind gr =
+  try Some (lookup_scheme kind gr) with Not_found -> None
 
 let all_schemes () = !scheme_map
diff --git a/tactics/declareScheme.mli b/tactics/declareScheme.mli
@@ -10,7 +10,7 @@
 
 open Names
 
-val declare_scheme : Libobject.locality -> string -> (inductive * GlobRef.t) -> unit
-val lookup_scheme : string -> inductive -> GlobRef.t
-val lookup_scheme_opt : string -> inductive -> GlobRef.t option
-val all_schemes : unit -> GlobRef.t CString.Map.t Indmap_env.t
+val declare_scheme : Libobject.locality -> string -> (GlobRef.t * GlobRef.t) -> unit
+val lookup_scheme : string -> GlobRef.t -> GlobRef.t
+val lookup_scheme_opt : string -> GlobRef.t -> GlobRef.t option
+val all_schemes : unit -> GlobRef.t CString.Map.t GlobRef.Map_env.t
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
@@ -104,7 +104,7 @@ let register_definition_scheme = ref (fun ~internal ~name ~const ~univs ?loc ()
   CErrors.anomaly (Pp.str "scheme registering not registered"))
 
 let lookup_scheme kind ind =
-  try Some (DeclareScheme.lookup_scheme kind ind) with Not_found -> None
+  try Some (DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind)) with Not_found -> None
 
 type schemes = {
   sch_eff : Evd.side_effects;
@@ -120,11 +120,11 @@ let redeclare_schemes { sch_eff = eff } =
   let fold c role accu = match role with
   | Evd.Schema (ind, kind) ->
     try
-      let _ = DeclareScheme.lookup_scheme kind ind in
+      let _ = DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind) in
       accu
     with Not_found ->
       let old = try String.Map.find kind accu with Not_found -> [] in
-      String.Map.add kind ((ind, GlobRef.ConstRef c) :: old) accu
+      String.Map.add kind ((GlobRef.IndRef ind, GlobRef.ConstRef c) :: old) accu
   in
   let schemes = Cmap_env.fold fold (Evd.seff_roles eff) String.Map.empty in
   let iter kind defs = List.iter (DeclareScheme.declare_scheme SuperGlobal kind) defs in
diff --git a/test-suite/success/SchemeSectionVariable.v b/test-suite/success/SchemeSectionVariable.v
@@ -0,0 +1,10 @@
+(** Test that scheme registrations for section variables require #[local]. *)
+
+Axiom foo : Type.
+
+Section S1.
+  Variable A : Type.
+  Fail #[export] Register Scheme foo as rew_r_dep for A.
+  Fail Global Register Scheme foo as rew_r_dep for A.
+  #[local] Register Scheme foo as rew_r_dep for A.
+End S1.
diff --git a/vernac/comSearch.ml b/vernac/comSearch.ml
@@ -56,7 +56,7 @@ let kind_searcher env = Decls.(function
   | IsDefinition Scheme ->
     let schemes = DeclareScheme.all_schemes () in
     let schemes = lazy begin
-      Indmap_env.fold (fun _ schemes acc ->
+      GlobRef.Map_env.fold (fun _ schemes acc ->
           CString.Map.fold (fun _ c acc ->
             GlobRef.Set_env.add c acc) schemes acc)
         schemes GlobRef.Set_env.empty
diff --git a/vernac/declare.ml b/vernac/declare.ml
@@ -484,7 +484,7 @@ let register_side_effect (c, body, role, univs) =
   in
   match role with
   | None -> ()
-  | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme SuperGlobal kind (ind, GlobRef.ConstRef c)
+  | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme SuperGlobal kind (GlobRef.IndRef ind, GlobRef.ConstRef c)
 
 let get_roles export eff =
   let eff = SideEff.obj eff in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
@@ -296,7 +296,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Register"; g = global; "as"; quid = qualid ->
           { VernacRegister(g, RegisterCoqlib quid) }
       | IDENT "Register"; IDENT "Scheme"; g = global; "as"; qid = qualid; IDENT "for"; g' = global ->
-        { VernacRegister(g, RegisterScheme {inductive = g'; scheme_kind = qid}) }
+        { VernacRegister(g, RegisterScheme {ref = g'; scheme_kind = qid}) }
       | IDENT "Register"; IDENT "Inline"; g = global ->
           { VernacRegister(g, RegisterInline) }
       | IDENT "Primitive"; id = ident_decl; typopt = OPT [ ":"; typ = lconstr -> { typ } ]; ":="; r = register_token ->
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
@@ -423,7 +423,7 @@ let do_mutual_induction_scheme ~register ?(force_mutual=false) env ?(isrec=true)
     | None -> ()
     | Some kind ->
       (* TODO locality *)
-      DeclareScheme.declare_scheme SuperGlobal (Ind_tables.scheme_kind_name kind) (ind, cst)
+      DeclareScheme.declare_scheme SuperGlobal (Ind_tables.scheme_kind_name kind) (GlobRef.IndRef ind, cst)
   in
   let () = List.iter2 declare listdecl l in
   let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) l in
@@ -555,7 +555,7 @@ let do_scheme_all_predicate ?all_depth ~declare_mind kn mib strpos sAll keyAll =
   let kn_nested = declare_mind ?all_depth mentry univs in
   (* register it *)
   let () = Array.iteri (fun i _ -> DeclareScheme.declare_scheme
-              SuperGlobal keyAll ((kn,i), GlobRef.IndRef (kn_nested,i))
+              SuperGlobal keyAll (GlobRef.IndRef (kn,i), GlobRef.IndRef (kn_nested,i))
             ) mib.mind_packets in
   kn_nested
 
@@ -581,7 +581,7 @@ let do_scheme_all_theorem kn mib kn_nested focus strpos sAllThm keyAllThm =
   let cinfo = Declare.CInfo.make ~name:fth_name ~typ:(None : (Evd.econstr option)) () in
   let fth_ref = Declare.declare_definition ~info:info ~cinfo:cinfo ~opaque:false ~body:(EConstr.of_constr thm) sigma in
   (* register it *)
-  let () = DeclareScheme.declare_scheme SuperGlobal keyAllThm ((kn,focus), fth_ref) in
+  let () = DeclareScheme.declare_scheme SuperGlobal keyAllThm (GlobRef.IndRef (kn,focus), fth_ref) in
   ()
 
 let do_all_forall ?(user_call_scheme=false) ?all_depth ~declare_mind kn strpos =
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
@@ -1278,11 +1278,11 @@ let pr_synpure_vernac_expr v =
         (keyword "Register" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
          ++ spc () ++ pr_qualid name)
     )
-  | VernacRegister (qid, RegisterScheme {inductive; scheme_kind}) ->
+  | VernacRegister (qid, RegisterScheme {ref; scheme_kind}) ->
     return (
       hov 2
         (keyword "Register" ++ spc() ++ keyword "Scheme" ++ spc() ++ pr_qualid qid ++ spc () ++ str "as"
-         ++ spc () ++ pr_qualid scheme_kind ++ spc() ++ str "for" ++ spc() ++ pr_qualid inductive)
+         ++ spc () ++ pr_qualid scheme_kind ++ spc() ++ str "for" ++ spc() ++ pr_qualid ref)
     )
   | VernacRegister (qid, RegisterInline) ->
     return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
@@ -375,13 +375,13 @@ let print_registered () =
 
 let print_registered_schemes () =
   let schemes = DeclareScheme.all_schemes() in
-  let pr_one_scheme ind (kind, c) =
-    pr_global c ++ str " registered as " ++ str kind ++ str " for " ++ pr_global (IndRef ind)
+  let pr_one_scheme key (kind, c) =
+    pr_global c ++ str " registered as " ++ str kind ++ str " for " ++ pr_global key
   in
-  let pr_schemes_of_ind (ind, schemes) =
-    prlist_with_sep fnl (pr_one_scheme ind) (CString.Map.bindings schemes)
+  let pr_schemes_of_ref (key, schemes) =
+    prlist_with_sep fnl (pr_one_scheme key) (CString.Map.bindings schemes)
   in
-  hov 0 (prlist_with_sep fnl pr_schemes_of_ind (Indmap_env.bindings schemes))
+  hov 0 (prlist_with_sep fnl pr_schemes_of_ref (GlobRef.Map_env.bindings schemes))
 
 let dump_universes output g =
   let open Univ in
@@ -2371,7 +2371,7 @@ let vernac_register ~atts qid r =
     else
       let local = Attributes.parse hint_locality_default_superglobal atts in
       Rocqlib.register_ref local (Libnames.string_of_qualid n) gr
-  | RegisterScheme { inductive; scheme_kind } ->
+  | RegisterScheme { ref; scheme_kind } ->
     let local = Attributes.parse hint_locality_default_superglobal atts in
     let scheme_kind_s = Libnames.string_of_qualid scheme_kind in
     (* Specific test for the All and AllForall keys, as there are an infinite number of them *)
@@ -2386,9 +2386,9 @@ let vernac_register ~atts qid r =
           || test_all "All_" scheme_kind_s || test_all "AllForall_" scheme_kind_s) then
       warn_unknown_scheme_kind ?loc:scheme_kind.loc scheme_kind
     in
-    let ind = Smartlocate.global_inductive_with_alias inductive in
-    Dumpglob.add_glob ?loc:inductive.loc (IndRef ind);
-    DeclareScheme.declare_scheme local scheme_kind_s (ind, gr)
+    let key = Smartlocate.global_with_alias ref in
+    Dumpglob.add_glob ?loc:ref.loc key;
+    DeclareScheme.declare_scheme local scheme_kind_s (key, gr)
 
 let vernac_library_attributes atts =
   if Global.is_curmod_library () && not (Lib.sections_are_opened ()) then
diff --git a/vernac/vernacexpr.mli b/vernac/vernacexpr.mli
@@ -304,7 +304,7 @@ type section_subset_expr =
 type register_kind =
   | RegisterInline
   | RegisterCoqlib of qualid
-  | RegisterScheme of { inductive : qualid; scheme_kind : qualid }
+  | RegisterScheme of { ref : qualid; scheme_kind : qualid }
 
 (** {6 Types concerning the module layer} *)
 

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+overlay elpi https://github.com/thomas-lamiaux/coq-elpi genScheme 21811`