feature(coq): support for inter-project composition of theories

Signed-off-by: Ali Caglayan <alizter@gmail.com>
ocaml · May 31, 2022 · 4aafc42 · 4aafc42
1 parent eb54e29
commit 4aafc42
Show file tree

Hide file tree

Showing 126 changed files with 888 additions and 342 deletions.
diff --git a/bin/coqtop.ml b/bin/coqtop.ml
@@ -96,6 +96,7 @@ let term =
               in
               let* (_ : unit * Dep.Fact.t Dep.Map.t) =
                 let deps =
+                  let boot_type = Resolve.Memo.return boot_type in
                   Dune_rules.Coq_rules.deps_of ~dir ~boot_type coq_module
                 in
                 Action_builder.run deps Eager

diff --git a/bin/import.ml b/bin/import.ml
@@ -28,6 +28,7 @@ module Workspace = Dune_rules.Workspace
 module Cached_digest = Dune_engine.Cached_digest
 module Targets = Dune_engine.Targets
 module Profile = Dune_rules.Profile
+module Resolve = Dune_rules.Resolve
 module Log = Dune_util.Log
 module Dune_rpc = Dune_rpc_private
 module Graph = Dune_graph.Graph