Skip to content

Commit 16a944a

Browse files
proux01proux01
committed
Drop support for Coq 8.15
1 parent 4c7c83d commit 16a944a

File tree

11 files changed

+2
-903
lines changed

11 files changed

+2
-903
lines changed

‎.github/workflows/main.yml‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ jobs:
1717
fail-fast: false
1818
matrix:
1919
coq_version:
20-
- '8.15'
2120
- '8.16'
2221
- '8.17'
2322
steps:

‎.github/workflows/nix-action-coq-8.15.yml‎

Lines changed: 0 additions & 670 deletions
This file was deleted.

‎.nix/config.nix‎

Lines changed: 0 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -38,14 +38,6 @@
3838
"coq-8.16".coqPackages = mcHBcommon // {
3939
coq.override.version = "8.16";
4040
};
41-
42-
"coq-8.15".coqPackages = mcHBcommon // {
43-
coq.override.version = "8.15";
44-
mathcomp.job = false;
45-
mathcomp-classical.job = false;
46-
mathcomp-analysis.job = false;
47-
mathcomp-infotheo.job = false;
48-
};
4941
};
5042
cachix.coq = {};
5143
cachix.coq-community = {};

‎HB/common/compat_815.elpi‎

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎HB/common/compat_all.elpi‎

Lines changed: 0 additions & 2 deletions
This file was deleted.

‎HB/common/log.elpi‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -159,7 +159,7 @@ env.import-module MPNice M :- std.do! [
159159

160160
pred coercion.declare i:coercion.
161161
coercion.declare C :- std.do! [
162-
compat.coercion.declare C,
162+
@global! => @reversible! => coq.coercion.declare C,
163163
C = coercion GR _ SRCGR TGTCL,
164164
coq.gref->id GR Name,
165165
log.private.log-vernac (log.private.coq.vernac.coercion Name SRCGR TGTCL),

‎coq-hierarchy-builder.opam‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ build: [ [ make "build"]
1212
[ make "test-suite" ] {with-test}
1313
]
1414
install: [ make "install" ]
15-
depends: [ "coq-elpi" { (>= "1.14" & < "1.20~") | = "dev" } ]
15+
depends: [ "coq-elpi" { (>= "1.15" & < "1.20~") | = "dev" } ]
1616
conflicts: [ "coq-hierarchy-builder-shim" ]
1717
synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
1818
description: """

‎structures.v‎

Lines changed: 0 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -244,8 +244,6 @@ Elpi Accumulate Db hb.db.
244244
the commands. To this end, we accumulate the DB first in each command to
245245
ensure the same dependencies and maximize cache hits. For instance, this
246246
can save a few (2 or 3) percents of total compilation time on MathComp. *)
247-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
248-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
249247
Elpi Accumulate lp:{{
250248

251249
main [str S] :- !,
@@ -274,8 +272,6 @@ Elpi Export HB.locate.
274272

275273
#[arguments(raw)] Elpi Command HB.about.
276274
Elpi Accumulate Db hb.db.
277-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
278-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
279275
Elpi Accumulate File "HB/common/stdpp.elpi".
280276
Elpi Accumulate File "HB/common/database.elpi".
281277
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -309,8 +305,6 @@ Elpi Export HB.about.
309305

310306
#[arguments(raw)] Elpi Command HB.howto.
311307
Elpi Accumulate Db hb.db.
312-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
313-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
314308
Elpi Accumulate File "HB/common/stdpp.elpi".
315309
Elpi Accumulate File "HB/common/database.elpi".
316310
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -352,8 +346,6 @@ Elpi Export HB.howto.
352346

353347
#[arguments(raw)] Elpi Command HB.status.
354348
Elpi Accumulate Db hb.db.
355-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
356-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
357349
Elpi Accumulate File "HB/common/stdpp.elpi".
358350
Elpi Accumulate File "HB/common/database.elpi".
359351
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -382,8 +374,6 @@ tred file.dot | xdot -
382374

383375
#[arguments(raw)] Elpi Command HB.graph.
384376
Elpi Accumulate Db hb.db.
385-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
386-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
387377
Elpi Accumulate File "HB/common/stdpp.elpi".
388378
Elpi Accumulate File "HB/common/database.elpi".
389379
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -432,8 +422,6 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
432422

433423
#[arguments(raw)] Elpi Command HB.mixin.
434424
Elpi Accumulate Db hb.db.
435-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
436-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
437425
Elpi Accumulate File "HB/common/stdpp.elpi".
438426
Elpi Accumulate File "HB/common/database.elpi".
439427
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -495,8 +483,6 @@ Elpi Export HB.mixin.
495483

496484
Elpi Tactic HB.pack_for.
497485
Elpi Accumulate Db hb.db.
498-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
499-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
500486
Elpi Accumulate File "HB/common/stdpp.elpi".
501487
Elpi Accumulate File "HB/common/database.elpi".
502488
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -519,8 +505,6 @@ Elpi Export HB.pack_for.
519505

520506
Elpi Tactic HB.pack.
521507
Elpi Accumulate Db hb.db.
522-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
523-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
524508
Elpi Accumulate File "HB/common/stdpp.elpi".
525509
Elpi Accumulate File "HB/common/database.elpi".
526510
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -605,8 +589,6 @@ HB.structure Definition StructureName params :=
605589

606590
#[arguments(raw)] Elpi Command HB.structure.
607591
Elpi Accumulate Db hb.db.
608-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
609-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
610592
Elpi Accumulate File "HB/common/stdpp.elpi".
611593
Elpi Accumulate File "HB/common/database.elpi".
612594
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -661,8 +643,6 @@ HB.instance Definition N Params := Factory.Build Params T …
661643

662644
#[arguments(raw)] Elpi Command HB.instance.
663645
Elpi Accumulate Db hb.db.
664-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
665-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
666646
Elpi Accumulate File "HB/common/stdpp.elpi".
667647
Elpi Accumulate File "HB/common/database.elpi".
668648
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -694,8 +674,6 @@ Elpi Export HB.instance.
694674

695675
#[arguments(raw)] Elpi Command HB.factory.
696676
Elpi Accumulate Db hb.db.
697-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
698-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
699677
Elpi Accumulate File "HB/common/stdpp.elpi".
700678
Elpi Accumulate File "HB/common/database.elpi".
701679
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -756,8 +734,6 @@ HB.end.
756734

757735
#[arguments(raw)] Elpi Command HB.builders.
758736
Elpi Accumulate Db hb.db.
759-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
760-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
761737
Elpi Accumulate File "HB/common/stdpp.elpi".
762738
Elpi Accumulate File "HB/common/database.elpi".
763739
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -782,8 +758,6 @@ Elpi Export HB.builders.
782758

783759
#[arguments(raw)] Elpi Command HB.end.
784760
Elpi Accumulate Db hb.db.
785-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
786-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
787761
Elpi Accumulate File "HB/common/stdpp.elpi".
788762
Elpi Accumulate File "HB/common/database.elpi".
789763
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -836,8 +810,6 @@ Export Algebra.Exports.
836810

837811
#[arguments(raw)] Elpi Command HB.export.
838812
Elpi Accumulate Db hb.db.
839-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
840-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
841813
Elpi Accumulate File "HB/common/stdpp.elpi".
842814
Elpi Accumulate File "HB/common/database.elpi".
843815
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -864,8 +836,6 @@ Elpi Export HB.export.
864836

865837
#[arguments(raw)] Elpi Command HB.reexport.
866838
Elpi Accumulate Db hb.db.
867-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
868-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
869839
Elpi Accumulate File "HB/common/stdpp.elpi".
870840
Elpi Accumulate File "HB/common/database.elpi".
871841
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -912,8 +882,6 @@ Notation foo := foo.body.
912882

913883
#[arguments(raw)] Elpi Command HB.lock.
914884
Elpi Accumulate Db hb.db.
915-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
916-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
917885
Elpi Accumulate File "HB/common/stdpp.elpi".
918886
Elpi Accumulate File "HB/common/database.elpi".
919887
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -963,8 +931,6 @@ HB.instance Definition _ : Ml ... T := ml.
963931

964932
#[arguments(raw)] Elpi Command HB.declare.
965933
Elpi Accumulate Db hb.db.
966-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
967-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
968934
Elpi Accumulate File "HB/common/stdpp.elpi".
969935
Elpi Accumulate File "HB/common/database.elpi".
970936
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1000,8 +966,6 @@ Elpi Export HB.declare.
1000966

1001967
#[arguments(raw)] Elpi Command HB.check.
1002968
Elpi Accumulate Db hb.db.
1003-
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
1004-
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
1005969
Elpi Accumulate File "HB/common/stdpp.elpi".
1006970
Elpi Accumulate File "HB/common/database.elpi".
1007971
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".

‎tests/about.v.out.15‎

Lines changed: 0 additions & 149 deletions
This file was deleted.

‎tests/compress_coe.v.out.15‎

Lines changed: 0 additions & 21 deletions
This file was deleted.

0 commit comments

Comments
 (0)