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

Reviewed-by: maximedenes

1 files changed, 17 insertions, 7 deletions

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