Skip to content

Commit 311dfa5

Browse files
authored
Merge pull request #190 from proux01/fix
Revert "[build] Fix missing deps in dune rule for All.v file"
2 parents d8cd504 + be54f13 commit 311dfa5

File tree

1 file changed

+2
-5
lines changed

1 file changed

+2
-5
lines changed

theories/dune

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,7 @@
11
(include_subdirs qualified)
2-
3-
; We omit All.v as not to block on rocq-core build
42
(coq.theory
53
(name Stdlib)
6-
(package rocq-stdlib)
7-
(modules :standard \ All))
4+
(package rocq-stdlib))
85

96
(env
107
(dev
@@ -13,5 +10,5 @@
1310

1411
(rule
1512
(targets All.v)
16-
(deps (package rocq-core) All.sh (source_tree .))
13+
(deps All.sh (source_tree .))
1714
(action (with-stdout-to %{targets} (run env bash ./All.sh))))

0 commit comments

Comments
 (0)