Merge PR #11307: Remove the hacks relying on hardwired libobject tags.

Reviewed-by: maximedenes

2 files changed, 20 insertions, 5 deletions

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 9a14f4d40f..c7581fb0e0 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -130,8 +130,8 @@ let dummy_constant cst = {
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant : constant_obj -> obj) =
-  declare_object { (default_object "CONSTANT") with
+let (objConstant : constant_obj Libobject.Dyn.tag) =
+  declare_object_full { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
     open_function = open_constant;
@@ -139,6 +139,8 @@ let (inConstant : constant_obj -> obj) =
     subst_function = ident_subst_function;
     discharge_function = discharge_constant }
 
+let inConstant v = Libobject.Dyn.Easy.inj v objConstant
+
 let update_tables c =
   Impargs.declare_constant_implicits c;
   Notation.declare_ref_arguments_scope Evd.empty (GlobRef.ConstRef c)
@@ -357,10 +359,12 @@ type variable_declaration =
 
 (* This object is only for things which iterate over objects to find
    variables (only Prettyp.print_context AFAICT) *)
-let inVariable : unit -> obj =
-  declare_object { (default_object "VARIABLE") with
+let objVariable : unit Libobject.Dyn.tag =
+  declare_object_full { (default_object "VARIABLE") with
     classify_function = (fun () -> Dispose)}
 
+let inVariable v = Libobject.Dyn.Easy.inj v objVariable
+
 let declare_variable ~name ~kind d =
   (* Variables are distinguished by only short names *)
   if Decls.variable_exists name then
@@ -497,4 +501,9 @@ module Internal = struct
     ; proof_entry_type = Some typ
     }, args
 
+  type nonrec constant_obj = constant_obj
+
+  let objVariable = objVariable
+  let objConstant = objConstant
+
 end
diff --git a/tactics/declare.mli b/tactics/declare.mli
index c646d2f85b..00c1e31717 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -131,7 +131,8 @@ val check_exists : Id.t -> unit
 (* Used outside this module only in indschemes *)
 exception AlreadyDeclared of (string option * Id.t)
 
-(* For legacy support, do not use *)
+(** {6 For legacy support, do not use}  *)
+
 module Internal : sig
 
   val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
@@ -145,4 +146,9 @@ module Internal : sig
 
   val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
 
+  type constant_obj
+
+  val objConstant : constant_obj Libobject.Dyn.tag
+  val objVariable : unit Libobject.Dyn.tag
+
 end