Merge PR #10442: Reify libobject containers

Reviewed-by: ejgallego
Reviewed-by: ppedrot

1 files changed, 27 insertions, 23 deletions

diff --git a/vernac/search.ml b/vernac/search.ml
index a7f1dd33c2..4af14e895d 100644
--- a/vernac/search.ml
+++ b/vernac/search.ml
@@ -75,30 +75,34 @@ let iter_hypothesis ?pstate glnum (fn : GlobRef.t -> env -> constr -> unit) =
 (* General search over declarations *)
 let iter_declarations (fn : GlobRef.t -> env -> constr -> unit) =
   let env = Global.env () in
-  let iter_obj (sp, kn) lobj = match object_tag lobj with
-  | "VARIABLE" ->
-    begin try
-      let decl = Global.lookup_named (basename sp) in
-      fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
-    with Not_found -> (* we are in a section *) () end
-  | "CONSTANT" ->
-    let cst = Global.constant_of_delta_kn kn in
-    let gr = ConstRef cst in
-    let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
+  let iter_obj (sp, kn) lobj = match lobj with
+  | AtomicObject o ->
+    begin match object_tag o with
+    | "VARIABLE" ->
+      begin try
+        let decl = Global.lookup_named (basename sp) in
+        fn (VarRef (NamedDecl.get_id decl)) env (NamedDecl.get_type decl)
+      with Not_found -> (* we are in a section *) () end
+    | "CONSTANT" ->
+      let cst = Global.constant_of_delta_kn kn in
+      let gr = ConstRef cst in
+      let (typ, _) = Typeops.type_of_global_in_context (Global.env ()) gr in
       fn gr env typ
-  | "INDUCTIVE" ->
-    let mind = Global.mind_of_delta_kn kn in
-    let mib = Global.lookup_mind mind in
-    let iter_packet i mip =
-      let ind = (mind, i) in
-      let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
-      let i = (ind, u) in
-      let typ = Inductiveops.type_of_inductive env i in
-      let () = fn (IndRef ind) env typ in
-      let len = Array.length mip.mind_user_lc in
-      iter_constructors ind u fn env len
-    in
-    Array.iteri iter_packet mib.mind_packets
+    | "INDUCTIVE" ->
+      let mind = Global.mind_of_delta_kn kn in
+      let mib = Global.lookup_mind mind in
+      let iter_packet i mip =
+        let ind = (mind, i) in
+        let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+        let i = (ind, u) in
+        let typ = Inductiveops.type_of_inductive env i in
+        let () = fn (IndRef ind) env typ in
+        let len = Array.length mip.mind_user_lc in
+        iter_constructors ind u fn env len
+      in
+      Array.iteri iter_packet mib.mind_packets
+    | _ -> ()
+    end
   | _ -> ()
   in
   try Declaremods.iter_all_segments iter_obj