Merge pull request #711 from LPCIC/fix-libobject

Fix libobject

Makefile

@@ -18,6 +18,7 @@ build:
 
 test-core:
 	$(call dune,runtest) tests
+	$(call dune,build) tests
 .PHONY: test-core
 
 test-apps:
@@ -26,6 +27,7 @@ test-apps:
 
 test:
 	$(call dune,runtest)
+	$(call dune,build) tests
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test
 

src/coq_elpi_programs.ml

@@ -461,19 +461,29 @@ let get ?(fail_if_not_exists=false) p =
         { sources_rev = Chunk.Base { hash = hash_cunit base; base }; units = Names.KNset.singleton kname }
     | _ -> assert false
 
+  let is_inside_current_library kn =
+    Names.DirPath.equal
+      (Lib.library_dp ())
+       (Names.KerName.modpath kn |> Names.ModPath.dp)
+
   let in_db : Names.Id.t -> snippet -> Libobject.obj =
     let open Libobject in
     let cache ((_,kn),{ program = name; code = p; _ }) =
       db_name_src := SLMap.add name (append_to_db name kn p) !db_name_src in
-    let import i (_,s as o) = if Int.equal i 1 || s.scope =  Coq_elpi_utils.SuperGlobal then cache o in
+    let load i ((_,kn),s as o) =
+      if Int.equal i 1 ||
+        (s.scope = Coq_elpi_utils.Global && is_inside_current_library kn) ||
+        s.scope = Coq_elpi_utils.SuperGlobal then cache o in
+    let import i (_,s as o) =
+      if Int.equal i 1 then cache o in
     declare_named_object @@ { (default_object "ELPI-DB") with
       classify_function = (fun { scope; program; _ } ->
         match scope with
         | Coq_elpi_utils.Local -> Dispose
         | Coq_elpi_utils.Regular -> Substitute
         | Coq_elpi_utils.Global -> Keep
         | Coq_elpi_utils.SuperGlobal -> Keep);
-      load_function  = import;
+      load_function  = load;
       cache_function  = cache;
       subst_function = (fun (_,o) -> o);
       open_function = simple_open import;