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.

5 files changed, 72 insertions, 24 deletions

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