Skip to content

Commit cf05e19

Browse files
committed
Dune refactoring: classify more deps as transitive
1 parent 6d1e75b commit cf05e19

4 files changed

Lines changed: 10 additions & 37 deletions

File tree

  • rocq-lens/Lens/Elpi
  • rocq-skylabs-brick/theories/lang/cpp
  • rocq-skylabs-iris/theories
  • rocq-skylabs-prelude/theories

rocq-lens/Lens/Elpi/dune

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,9 @@
33
(generate_project_file)
44
(theories
55
Lens
6-
elpi
7-
elpi_elpi
86
elpi.apps.derive
97
; transitive dependencies
10-
elpi.apps.derive.elpi
8+
elpi elpi.apps.derive.elpi elpi_elpi
119
)
1210
(package rocq-lens-elpi))
1311

rocq-skylabs-brick/theories/lang/cpp/dune

Lines changed: 4 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -5,25 +5,13 @@
55
(plugins rocq-skylabs-brick.plugin)
66
(generate_project_file)
77
(theories
8-
Stdlib
9-
stdpp
10-
skylabs.upoly
11-
elpi
12-
elpi_elpi
13-
elpi.apps.locker
14-
elpi.apps.NES
15-
Lens
16-
Lens.Elpi
17-
Ltac2
18-
skylabs.ltac2.extra
19-
skylabs.prelude
20-
iris
21-
Flocq
228
skylabs.iris.extra
9+
Flocq
2310
Equations
2411
Equations.Prop
2512
Equations.Type
2613
; transitive dependencies
27-
elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
28-
elpi.apps.locker.elpi
14+
Lens Lens.Elpi Ltac2 Stdlib elpi elpi.apps.NES elpi.apps.NES.elpi
15+
elpi.apps.derive elpi.apps.derive.elpi elpi.apps.locker elpi.apps.locker.elpi
16+
elpi_elpi iris skylabs.ltac2.extra skylabs.prelude skylabs.upoly stdpp
2917
))

rocq-skylabs-iris/theories/dune

Lines changed: 3 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -4,20 +4,10 @@
44
(package rocq-skylabs-iris)
55
(generate_project_file)
66
(theories
7-
Stdlib
8-
stdpp
9-
skylabs.upoly
10-
elpi
11-
elpi_elpi
12-
elpi.apps.locker
13-
elpi.apps.NES
14-
Lens
15-
Lens.Elpi
16-
Ltac2
17-
skylabs.ltac2.extra
187
skylabs.prelude
198
iris
209
; transitive dependencies
21-
elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
22-
elpi.apps.locker.elpi
10+
Lens Lens.Elpi Ltac2 Stdlib elpi elpi.apps.NES elpi.apps.NES.elpi
11+
elpi.apps.derive elpi.apps.derive.elpi elpi.apps.locker elpi.apps.locker.elpi
12+
elpi_elpi skylabs.ltac2.extra skylabs.upoly stdpp
2313
))

rocq-skylabs-prelude/theories/dune

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,20 +4,17 @@
44
(package rocq-skylabs-prelude)
55
(generate_project_file)
66
(theories
7-
Stdlib
87
stdpp
98
skylabs.upoly
109
elpi
11-
elpi_elpi
1210
elpi.apps.locker
1311
elpi.apps.NES
1412
Lens
1513
Lens.Elpi
16-
Ltac2
1714
skylabs.ltac2.extra
1815
; transitive dependencies
19-
elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
20-
elpi.apps.locker.elpi
16+
Ltac2 Stdlib elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
17+
elpi.apps.locker.elpi elpi_elpi
2118
))
2219

2320
; Copy dependencies --- typically Elpi files needed for `From ⋯ Extra

0 commit comments

Comments
 (0)