Remove the hacks relying on hardwired libobject tags.

The patch is done in a minimal way. The hacks are turned into a new kind of
safer hacks, but hacks nonetheless. They should go away at some point, but
the current patch is focussed on the removal of Libobject cruft, not making
the dirty code of its upper-layer callers any cleaner.

11 files changed, 112 insertions, 41 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f7f2bcdcff..92db2cc78b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -254,7 +254,9 @@ let ppenvwithcst e = pp
 
 let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
-let ppobj obj = Format.print_string (Libobject.object_tag obj)
+let ppobj obj =
+  let Libobject.Dyn.Dyn (tag, _) = obj in
+  Format.print_string (Libobject.Dyn.repr tag)
 
 let cnt = ref 0
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 54c23ff2d5..28d0654444 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -82,8 +82,6 @@ and objects = (Names.Id.t * t) list
 
 and substitutive_objects = MBId.t list * algebraic_objects
 
-let object_tag (Dyn.Dyn (t, _)) = Dyn.repr t
-
 module DynMap = Dyn.Map (struct type 'a t = 'a object_declaration end)
 
 let cache_tab = ref DynMap.empty
diff --git a/library/libobject.mli b/library/libobject.mli
index c83ad4086a..c25345994a 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -127,8 +127,6 @@ val declare_object_full :
 val declare_object :
   'a object_declaration -> ('a -> obj)
 
-val object_tag : obj -> string
-
 val cache_object : object_name * obj -> unit
 val load_object : int -> object_name * obj -> unit
 val open_object : int -> object_name * obj -> unit
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 35110552ab..2dc3e8a934 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -26,19 +26,29 @@ open Common
 (*S Part I: computing Coq environment. *)
 (***************************************)
 
+(* FIXME: this is a Libobject hack that should be removed. *)
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> (Label.t * structure_field_body) option end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> None
+
 let toplevel_env () =
   let get_reference = function
-    | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
-      let mp,l = KerName.repr kn in
-            begin match Libobject.object_tag o with
-            | "CONSTANT" ->
+  | (_,kn), Lib.Leaf Libobject.AtomicObject o ->
+    let mp,l = KerName.repr kn in
+    let handler =
+      DynHandle.add Declare.Internal.objConstant begin fun _ ->
         let constant = Global.lookup_constant (Constant.make1 kn) in
         Some (l, SFBconst constant)
-            | "INDUCTIVE" ->
+      end @@
+      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
         let inductive = Global.lookup_mind (MutInd.make1 kn) in
         Some (l, SFBmind inductive)
-            | _ -> None
-      end
+      end @@
+      DynHandle.empty
+    in
+    handle handler o
     | (_,kn), Lib.Leaf Libobject.ModuleObject _ ->
       let mp,l = KerName.repr kn in
       let modl = Global.lookup_module (MPdot (mp, l)) in
diff --git a/tactics/declare.ml b/tactics/declare.ml
index da4de3df77..133b26a99d 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 =
   (* Constr raisonne sur les noms courts *)
   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
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2375028541..7dd53564cc 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -60,9 +60,9 @@ let cache_inductive ((sp, kn), names) =
 let discharge_inductive ((sp, kn), names) =
   Some names
 
-let inInductive : inductive_obj -> Libobject.obj =
+let objInductive : inductive_obj Libobject.Dyn.tag =
   let open Libobject in
-  declare_object {(default_object "INDUCTIVE") with
+  declare_object_full {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
     open_function = open_inductive;
@@ -71,6 +71,7 @@ let inInductive : inductive_obj -> Libobject.obj =
     discharge_function = discharge_inductive;
   }
 
+let inInductive v = Libobject.Dyn.Easy.inj v objInductive
 
 let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
 
@@ -212,3 +213,9 @@ let declare_mutual_inductive_with_eliminations ?(primitive_expected=false) mie p
   if mie.mind_entry_private == None
   then Indschemes.declare_default_schemes mind;
   mind
+
+module Internal =
+struct
+  type nonrec inductive_obj = inductive_obj
+  let objInductive = objInductive
+end
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index df8895a999..17647d50aa 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -21,3 +21,12 @@ val declare_mutual_inductive_with_eliminations
   -> UnivNames.universe_binders
   -> one_inductive_impls list
   -> Names.MutInd.t
+
+(** {6 For legacy support, do not use}  *)
+module Internal :
+sig
+
+type inductive_obj
+val objInductive : inductive_obj Libobject.Dyn.tag
+
+end
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index eb7b28f15b..ec8658d939 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -670,25 +670,35 @@ let gallina_print_syntactic_def env kn =
      Constrextern.without_specific_symbols
        [Notation.SynDefRule kn] (pr_glob_constr_env env) c)
 
-let gallina_print_leaf_entry env sigma with_values ((sp,kn as oname),lobj) =
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t option end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> None
+
+(* TODO: this kind of feature should not rely on the Libobject stack. There is
+   no reason that an object in the stack corresponds to a user-facing
+   declaration. It may have been so at the time this was written, but this
+   needs to be done in a more principled way. *)
+let gallina_print_leaf_entry env sigma with_values ((sp, kn),lobj) =
   let sep = if with_values then " = " else " : " in
   match lobj with
   | AtomicObject o ->
-    let tag = object_tag o in
-    begin match (oname,tag) with
-      | (_,"VARIABLE") ->
+    let handler =
+      DynHandle.add Declare.Internal.objVariable begin fun _ ->
           (* Outside sections, VARIABLES still exist but only with universes
              constraints *)
           (try Some(print_named_decl env sigma (basename sp)) with Not_found -> None)
-      | (_,"CONSTANT") ->
+      end @@
+      DynHandle.add Declare.Internal.objConstant begin fun _ ->
           Some (print_constant with_values sep (Constant.make1 kn) None)
-      | (_,"INDUCTIVE") ->
+      end @@
+      DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
           Some (gallina_print_inductive (MutInd.make1 kn) None)
-      | (_,("AUTOHINT"|"GRAMMAR"|"SYNTAXCONSTANT"|"PPSYNTAX"|"TOKEN"|"CLASS"|
-            "COERCION"|"REQUIRE"|"END-SECTION"|"STRUCTURE")) -> None
-      (* To deal with forgotten cases... *)
-      | (_,s) -> None
-    end
+      end @@
+      DynHandle.empty
+    in
+    handle handler o
   | ModuleObject _ ->
     let (mp,l) = KerName.repr kn in
     Some (print_module with_values ~mod_ops:Declaremods.mod_ops (MPdot (mp,l)))
@@ -777,11 +787,18 @@ let print_full_context env sigma =
 let print_full_context_typ env sigma =
   print_context env sigma false None (Lib.contents ())
 
+module DynHandleF = Libobject.Dyn.Map(struct type 'a t = 'a -> Pp.t end)
+
+let handleF h (Libobject.Dyn.Dyn (tag, o)) = match DynHandleF.find tag h with
+| f -> f o
+| exception Not_found -> mt ()
+
+(* TODO: see the comment for {!gallina_print_leaf_entry} *)
 let print_full_pure_context env sigma =
   let rec prec = function
   | ((_,kn),Lib.Leaf AtomicObject lobj)::rest ->
-      let pp = match object_tag lobj with
-      | "CONSTANT" ->
+    let handler =
+      DynHandleF.add Declare.Internal.objConstant begin fun _ ->
           let con = Global.constant_of_delta_kn kn in
           let cb = Global.lookup_constant con in
           let typ = cb.const_type in
@@ -804,12 +821,16 @@ let print_full_pure_context env sigma =
                  str "Primitive " ++
                    print_basename con ++ str " : " ++ cut () ++ pr_ltype_env env sigma typ)
           ++ str "." ++ fnl () ++ fnl ()
-      | "INDUCTIVE" ->
+      end @@
+      DynHandleF.add DeclareInd.Internal.objInductive begin fun _ ->
           let mind = Global.mind_of_delta_kn kn in
           let mib = Global.lookup_mind mind in
           pr_mutual_inductive_body (Global.env()) mind mib None ++
             str "." ++ fnl () ++ fnl ()
-      | _ -> mt () in
+      end @@
+      DynHandleF.empty
+    in
+    let pp = handleF handler lobj in
       prec rest ++ pp
   | ((_,kn),Lib.Leaf ModuleObject _)::rest ->
           (* TODO: make it reparsable *)
diff --git a/vernac/search.ml b/vernac/search.ml
index 364dae7152..b8825c3b29 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -71,6 +71,14 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
   let pfctxt = named_context e in
   iter_named_context_name_type iter_hyp pfctxt
 
+(* FIXME: this is a Libobject hack that should be replaced with a proper
+   registration mechanism. *)
+module DynHandle = Libobject.Dyn.Map(struct type 'a t = 'a -> unit end)
+
+let handle h (Libobject.Dyn.Dyn (tag, o)) = match DynHandle.find tag h with
+| f -> f o
+| exception Not_found -> ()
+
 (* General search over declarations *)
 let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
@@ -78,13 +86,14 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
     (Environ.named_context env);
   let iter_obj (sp, kn) lobj = match lobj with
     | AtomicObject o ->
-      begin match object_tag o with
-        | "CONSTANT" ->
+      let handler =
+        DynHandle.add Declare.Internal.objConstant begin fun _ ->
           let cst = Global.constant_of_delta_kn kn in
           let gr = GlobRef.ConstRef cst in
           let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
           fn gr env typ
-        | "INDUCTIVE" ->
+        end @@
+        DynHandle.add DeclareInd.Internal.objInductive begin fun _ ->
           let mind = Global.mind_of_delta_kn kn in
           let mib = Global.lookup_mind mind in
           let iter_packet i mip =
@@ -97,8 +106,10 @@ let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
             iter_constructors ind u fn env len
           in
           Array.iteri iter_packet mib.mind_packets
-        | _ -> ()
-      end
+        end @@
+        DynHandle.empty
+      in
+      handle handler o
     | _ -> ()
   in
   try Declaremods.iter_all_segments iter_obj
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 5226c2ba65..833c279320 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -19,11 +19,9 @@ DeclareObl
 Canonical
 RecLemmas
 Library
-Prettyp
 Lemmas
 Class
 Auto_ind_decl
-Search
 Indschemes
 Obligations
 ComDefinition
@@ -31,6 +29,8 @@ Classes
 ComPrimitive
 ComAssumption
 DeclareInd
+Search
+Prettyp
 ComInductive
 ComFixpoint
 ComProgramFixpoint