Merge PR #18529: Remove Dyn.anonymous

Reviewed-by: ppedrot
Reviewed-by: ejgallego
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>

clib/dyn.ml

@@ -42,7 +42,6 @@ sig
   type t = Dyn : 'a tag * 'a -> t
 
   val create : string -> 'a tag
-  val anonymous : int -> 'a tag
   val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
   val repr : 'a tag -> string
 
@@ -104,14 +103,6 @@ module Self : PreS = struct
     dyntab := Int.Map.add hash s !dyntab;
     hash
 
-  let anonymous n =
-    if Int.Map.mem n !dyntab then begin
-      Printf.eprintf "Dynamic tag collision: %d\n%!" n;
-      assert false
-    end;
-    dyntab := Int.Map.add n "<anonymous>" !dyntab;
-    n
-
   let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option =
     fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None
 

clib/dyn.mli

@@ -52,12 +52,6 @@ sig
       Type names are hashed, so [create] may raise even if no type with
       the exact same name was registered due to a collision. *)
 
-  val anonymous : int -> 'a tag
-  (** [anonymous i] returns a tag describing an [i]-th anonymous type.
-      If [anonymous] is not used together with [create], [max_int] anonymous types
-      are available.
-      [anonymous] raises an exception if [i] is already registered. *)
-
   val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option
   (** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *)
 

clib/exninfo.ml

@@ -60,7 +60,7 @@ let rec find_and_remove_assoc (i : int) = function
 type backtrace = Printexc.raw_backtrace
 let backtrace_to_string = Printexc.raw_backtrace_to_string
 
-let backtrace_info : backtrace t = make ()
+let backtrace_info : backtrace t = make "exninfo_backtrace"
 
 let is_recording = ref false
 

clib/exninfo.mli

@@ -19,7 +19,7 @@ type info
 type iexn = exn * info
 (** Information-wearing exceptions *)
 
-val make : unit -> 'a t
+val make : string -> 'a t
 (** Create a new piece of information. *)
 
 val null : info

clib/store.ml

@@ -20,7 +20,7 @@ module type S =
 sig
   type t
   type 'a field
-  val field : unit -> 'a field
+  val field : string -> 'a field
   val empty : t
   val set : t -> 'a field -> 'a -> t
   val get : t -> 'a field -> 'a option
@@ -36,11 +36,7 @@ struct
   type t = Map.t
   type 'a field = 'a Dyn.tag
 
-  let next = ref 0
-  let field () =
-    let f = Dyn.anonymous !next in
-    incr next;
-    f
+  let field = Dyn.create
 
   let empty =
     Map.empty

clib/store.mli

@@ -19,8 +19,8 @@ sig
   type 'a field
   (** Type of field of such stores *)
 
-  val field : unit -> 'a field
-  (** Create a new field *)
+  val field : string -> 'a field
+  (** Create a new field. See also [Dyn.create]. *)
 
   val empty : t
   (** Empty store *)

dev/ci/user-overlays/18529-SkySkimmer-dyn-no-anon.sh

@@ -0,0 +1,5 @@
+overlay tactician https://github.com/SkySkimmer/coq-tactician dyn-no-anon 18529
+
+overlay vscoq https://github.com/SkySkimmer/vscoq dyn-no-anon 18529
+
+overlay waterproof https://github.com/SkySkimmer/coq-waterproof dyn-no-anon 18529

lib/loc.ml

@@ -91,7 +91,7 @@ let map f (l,x) = (l, f x)
 
 (** Exceptions *)
 
-let location : t Exninfo.t = Exninfo.make ()
+let location : t Exninfo.t = Exninfo.make "location"
 
 let add_loc e loc = Exninfo.add e location loc
 let get_loc e = Exninfo.get e location

lib/stateid.ml

@@ -19,7 +19,7 @@ let of_int id = id
 let to_int id = id
 let newer_than id1 id2 = id1 > id2
 
-let state_id_info : (t * t) Exninfo.t = Exninfo.make ()
+let state_id_info : (t * t) Exninfo.t = Exninfo.make "stateid"
 let add exn ~valid id =
   Exninfo.add exn state_id_info (valid, id)
 let get exn = Exninfo.get exn state_id_info

plugins/ltac/tacinterp.ml

@@ -140,11 +140,11 @@ let name_vfun appl vle =
 
 module TacStore = Geninterp.TacStore
 
-let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field ()
+let f_avoid_ids : Id.Set.t TacStore.field = TacStore.field "f_avoid_ids"
 (* ids inherited from the call context (needed to get fresh ids) *)
-let f_debug : debug_info TacStore.field = TacStore.field ()
-let f_trace : ltac_trace TacStore.field = TacStore.field ()
-let f_loc : Loc.t TacStore.field = TacStore.field ()
+let f_debug : debug_info TacStore.field = TacStore.field "f_debug"
+let f_trace : ltac_trace TacStore.field = TacStore.field "f_trace"
+let f_loc : Loc.t TacStore.field = TacStore.field "f_loc"
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign = Geninterp.interp_sign =

plugins/ltac/tactic_debug.ml

@@ -15,7 +15,7 @@ open Names
 open Pp
 open Tacexpr
 
-let (ltac_trace_info : ltac_stack Exninfo.t) = Exninfo.make ()
+let (ltac_trace_info : ltac_stack Exninfo.t) = Exninfo.make "ltac_trace"
 
 let prtac x =
   let env = Global.env () in

plugins/ltac2/tac2bt.ml

@@ -11,9 +11,9 @@
 open Tac2expr
 open Proofview.Notations
 
-let backtrace_evd : backtrace Evd.Store.field = Evd.Store.field ()
+let backtrace_evd : backtrace Evd.Store.field = Evd.Store.field "ltac2_trace"
 
-let backtrace : backtrace Exninfo.t = Exninfo.make ()
+let backtrace : backtrace Exninfo.t = Exninfo.make "ltac2_trace"
 
 let print_ltac2_backtrace = ref false
 

plugins/ltac2/tac2core.ml

@@ -196,7 +196,7 @@ let err_division_by_zero =
 
 let thaw f = Tac2ffi.apply f [v_unit]
 
-let fatal_flag : unit Exninfo.t = Exninfo.make ()
+let fatal_flag : unit Exninfo.t = Exninfo.make "fatal_flag"
 
 let has_fatal_flag info = match Exninfo.get info fatal_flag with
   | None -> false

plugins/ltac2/tac2intern.ml

@@ -35,7 +35,7 @@ let t_pattern = coq_type "pattern"
 let t_bool = coq_type "bool"
 
 let ltac2_env : Tac2typing_env.t Genintern.Store.field =
-  Genintern.Store.field ()
+  Genintern.Store.field "ltac2_env"
 
 let drop_ltac2_env store =
   Genintern.Store.remove store ltac2_env

plugins/ssr/ssrcommon.ml

@@ -1350,12 +1350,13 @@ let unprotecttac =
 module type StateType = sig
   type state
   val init : state
+  val name : string
 end
 
 module MakeState(S : StateType) = struct
 
 let state_field : S.state Proofview_monad.StateStore.field =
-  Proofview_monad.StateStore.field ()
+  Proofview_monad.StateStore.field S.name
 
 (* FIXME: should not inject fresh_state, but initialize it at the beginning *)
 let lift_upd_state upd s =

plugins/ssr/ssrcommon.mli

@@ -348,6 +348,7 @@ val tacMK_SSR_CONST : string -> EConstr.t Proofview.tactic
 module type StateType = sig
   type state
   val init : state
+  val name : string
 end
 
 module MakeState(S : StateType) : sig

plugins/ssr/ssripats.ml

@@ -151,6 +151,7 @@ let empty_state = {
 include Ssrcommon.MakeState(struct
   type state = istate
   let init = empty_state
+  let name = "ssripats"
 end)
 
 let print_name_seed env sigma = function

plugins/ssr/ssrview.ml

@@ -85,6 +85,7 @@ type vstate = {
 include Ssrcommon.MakeState(struct
   type state = vstate option
   let init = None
+  let name = "ssrview"
 end)
 
 let vsINIT ~view ~subject_name ~to_clear =

proofs/proof.ml

@@ -44,11 +44,7 @@ type 'a focus_condition =
   | CondDone     of bool * 'a focus_kind
   | CondEndStack of        'a focus_kind (* loose_end is false here *)
 
-let next_kind = ref 0
-let new_focus_kind () =
-  let r = !next_kind in
-  incr next_kind;
-  FocusKind.anonymous r
+let new_focus_kind = FocusKind.create
 
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.*)
@@ -273,7 +269,7 @@ let rec maximal_unfocus k p =
 (*** Proof Creation/Termination ***)
 
 (* [end_of_stack] is unfocused by return to close every loose focus. *)
-let end_of_stack_kind = new_focus_kind ()
+let end_of_stack_kind = new_focus_kind "end_of_stack"
 let end_of_stack = CondEndStack end_of_stack_kind
 
 let unfocused = is_last_focus end_of_stack_kind

proofs/proof.mli

@@ -99,7 +99,7 @@ val return : ?pid:Names.Id.t -> t -> Evd.evar_map
     of the declarative mode where sub-tactics must be aware of the current
     induction argument. *)
 type 'a focus_kind
-val new_focus_kind : unit -> 'a focus_kind
+val new_focus_kind : string -> 'a focus_kind
 
 (* To be authorized to unfocus one must meet the condition prescribed by
     the action which focused.

proofs/proof_bullet.ml

@@ -84,7 +84,7 @@ module Strict = struct
 
 
   (* spiwack: we need only one focus kind as we keep a stack of (distinct!) bullets *)
-  let bullet_kind = (new_focus_kind () : t list focus_kind)
+  let bullet_kind = (new_focus_kind "bullet_kind" : t list focus_kind)
   let bullet_cond = done_cond ~loose_end:true bullet_kind
 
   (* spiwack: as it is bullets are reset (locally) by *any* non-bullet focusing command

stm/partac.ml

@@ -97,7 +97,7 @@ end = struct (* {{{ *)
       t_assign := Some (RespKilled t_goalno)
     | _ -> ()
 
-  let command_focus = Proof.new_focus_kind ()
+  let command_focus = Proof.new_focus_kind "partac_focus"
   let focus_cond = Proof.no_cond command_focus
 
   let state = ref None

tactics/hints.ml

@@ -1730,7 +1730,7 @@ let print_mp mp =
 
 let is_imported h = try KNmap.find h.uid !statustable with Not_found -> true
 
-let hint_trace = Evd.Store.field ()
+let hint_trace = Evd.Store.field "hint_trace"
 
 let log_hint h =
   let open Proofview.Notations in

vernac/egramcoq.ml

@@ -619,7 +619,7 @@ let extend_constr state forpat ng =
   in
   List.fold_left fold ([], state) ng.notgram_prods
 
-let constr_levels = GramState.field ()
+let constr_levels = GramState.field "constr_levels"
 
 let is_disjunctive_pattern_rule ng =
   String.is_sub "( _ | " (snd ng.notgram_notation) 0

vernac/vernacentries.ml

@@ -1501,7 +1501,7 @@ let vernac_existing_class id =
 (***********)
 (* Solving *)
 
-let command_focus = Proof.new_focus_kind ()
+let command_focus = Proof.new_focus_kind "command_focus"
 let focus_command_cond = Proof.no_cond command_focus
 
 let vernac_set_end_tac pstate tac =
@@ -2132,7 +2132,7 @@ let vernac_unfocused ~pstate =
 (* "{" focuses on the first goal, "n: {" focuses on the n-th goal
     "}" unfocuses, provided that the proof of the goal has been completed.
 *)
-let subproof_kind = Proof.new_focus_kind ()
+let subproof_kind = Proof.new_focus_kind "subproof"
 let subproof_cond = Proof.done_cond subproof_kind
 
 let vernac_subproof gln ~pstate =