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

Reviewed-by: maximedenes

1 files changed, 13 insertions, 4 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