Skip to content

Commit 744c0a6

Browse files
CohenCyrilCohenCyril
committed
trying to fix it for 8.15
1 parent b749f90 commit 744c0a6

File tree

3 files changed

+20
-3
lines changed

3 files changed

+20
-3
lines changed

‎.nix/config.nix‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,6 @@
1919
in {
2020
"coq-mcHB-8.16".coqPackages = {
2121
coq.override.version = "8.16";
22-
coq-elpi.override.version = "master";
2322
mathcomp-analysis.override.version = "coq816";
2423
} // mcHBcommon;
2524

@@ -29,7 +28,6 @@
2928

3029
"coq-8.16".coqPackages = {
3130
coq.override.version = "8.16";
32-
coq-elpi.override.version = "master";
3331
mathcomp.override.version = "mathcomp-1.15.0";
3432
};
3533
"coq-8.15".coqPackages = {

‎.nix/coq-overlays/coq-elpi/default.nix‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,15 @@ in mkCoqDerivation {
1515
owner = "LPCIC";
1616
inherit version;
1717
defaultVersion = lib.switch coq.coq-version [
18+
{ case = "8.16"; out = "1.15.3"; }
1819
{ case = "8.15"; out = "1.14.0"; }
1920
{ case = "8.14"; out = "1.11.2"; }
2021
{ case = "8.13"; out = "1.11.1"; }
2122
{ case = "8.12"; out = "1.8.3_8.12"; }
2223
{ case = "8.11"; out = "1.6.3_8.11"; }
2324
] null;
24-
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
25+
release."1.15.3".sha256 = "0vsgpflvfbbpbri3xfdhkz24bc36gy90f0mh0nr9ml6pqyp0ygji";
26+
release."1.14.0".sha256 = "1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
2527
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
2628
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
2729
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";

‎structures.v‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,7 @@ compress X X.
248248

249249
#[arguments(raw)] Elpi Command HB.locate.
250250
Elpi Accumulate Db hb.db.
251+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
251252
Elpi Accumulate lp:{{
252253

253254
main _ :- coq.version _ _ N _, N < 13, !,
@@ -277,6 +278,7 @@ Elpi Export HB.locate.
277278
*)
278279

279280
#[arguments(raw)] Elpi Command HB.about.
281+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
280282
Elpi Accumulate File "HB/common/stdpp.elpi".
281283
Elpi Accumulate File "HB/common/database.elpi".
282284
Elpi Accumulate File "HB/common/utils.elpi".
@@ -302,6 +304,7 @@ Elpi Export HB.about.
302304
*)
303305

304306
#[arguments(raw)] Elpi Command HB.status.
307+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
305308
Elpi Accumulate File "HB/common/stdpp.elpi".
306309
Elpi Accumulate File "HB/common/database.elpi".
307310
Elpi Accumulate File "HB/common/utils.elpi".
@@ -328,6 +331,7 @@ tred file.dot | xdot -
328331
*)
329332

330333
#[arguments(raw)] Elpi Command HB.graph.
334+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
331335
Elpi Accumulate File "HB/common/stdpp.elpi".
332336
Elpi Accumulate File "HB/common/database.elpi".
333337
Elpi Accumulate File "HB/common/utils.elpi".
@@ -374,6 +378,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
374378
*)
375379

376380
#[arguments(raw)] Elpi Command HB.mixin.
381+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
377382
Elpi Accumulate File "HB/common/stdpp.elpi".
378383
Elpi Accumulate File "HB/common/database.elpi".
379384
Elpi Accumulate File "HB/common/utils.elpi".
@@ -434,6 +439,7 @@ Elpi Export HB.mixin.
434439

435440
Elpi Tactic HB.pack_for.
436441
Elpi Accumulate Db hb.db.
442+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
437443
Elpi Accumulate File "HB/common/stdpp.elpi".
438444
Elpi Accumulate File "HB/common/database.elpi".
439445
Elpi Accumulate File "HB/common/utils.elpi".
@@ -454,6 +460,7 @@ Elpi Export HB.pack_for.
454460

455461
Elpi Tactic HB.pack.
456462
Elpi Accumulate Db hb.db.
463+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
457464
Elpi Accumulate File "HB/common/stdpp.elpi".
458465
Elpi Accumulate File "HB/common/database.elpi".
459466
Elpi Accumulate File "HB/common/utils.elpi".
@@ -535,6 +542,7 @@ HB.structure Definition StructureName params :=
535542
*)
536543

537544
#[arguments(raw)] Elpi Command HB.structure.
545+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
538546
Elpi Accumulate File "HB/common/stdpp.elpi".
539547
Elpi Accumulate File "HB/common/database.elpi".
540548
Elpi Accumulate File "HB/common/utils.elpi".
@@ -587,6 +595,7 @@ HB.instance Definition N Params := Factory.Build Params T …
587595
*)
588596

589597
#[arguments(raw)] Elpi Command HB.instance.
598+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
590599
Elpi Accumulate File "HB/common/stdpp.elpi".
591600
Elpi Accumulate File "HB/common/database.elpi".
592601
Elpi Accumulate File "HB/common/utils.elpi".
@@ -616,6 +625,7 @@ Elpi Export HB.instance.
616625
(** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)
617626

618627
#[arguments(raw)] Elpi Command HB.factory.
628+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
619629
Elpi Accumulate File "HB/common/stdpp.elpi".
620630
Elpi Accumulate File "HB/common/database.elpi".
621631
Elpi Accumulate File "HB/common/utils.elpi".
@@ -674,6 +684,7 @@ HB.end.
674684
*)
675685

676686
#[arguments(raw)] Elpi Command HB.builders.
687+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
677688
Elpi Accumulate File "HB/common/stdpp.elpi".
678689
Elpi Accumulate File "HB/common/database.elpi".
679690
Elpi Accumulate File "HB/common/utils.elpi".
@@ -696,6 +707,7 @@ Elpi Export HB.builders.
696707

697708

698709
#[arguments(raw)] Elpi Command HB.end.
710+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
699711
Elpi Accumulate File "HB/common/stdpp.elpi".
700712
Elpi Accumulate File "HB/common/database.elpi".
701713
Elpi Accumulate File "HB/common/utils.elpi".
@@ -746,6 +758,7 @@ Export Algebra.Exports.
746758
*)
747759

748760
#[arguments(raw)] Elpi Command HB.export.
761+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
749762
Elpi Accumulate File "HB/common/stdpp.elpi".
750763
Elpi Accumulate File "HB/common/database.elpi".
751764
Elpi Accumulate File "HB/common/utils.elpi".
@@ -770,6 +783,7 @@ Elpi Export HB.export.
770783
(a module which is not closed yet) *)
771784

772785
#[arguments(raw)] Elpi Command HB.reexport.
786+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
773787
Elpi Accumulate File "HB/common/stdpp.elpi".
774788
Elpi Accumulate File "HB/common/database.elpi".
775789
Elpi Accumulate File "HB/common/utils.elpi".
@@ -814,6 +828,7 @@ Notation foo := foo.body.
814828
*)
815829

816830
#[arguments(raw)] Elpi Command HB.lock.
831+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
817832
Elpi Accumulate File "HB/common/stdpp.elpi".
818833
Elpi Accumulate File "HB/common/database.elpi".
819834
Elpi Accumulate File "HB/common/utils.elpi".
@@ -861,6 +876,7 @@ HB.instance Definition _ : Ml ... T := ml.
861876
*)
862877

863878
#[arguments(raw)] Elpi Command HB.declare.
879+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
864880
Elpi Accumulate File "HB/common/stdpp.elpi".
865881
Elpi Accumulate File "HB/common/database.elpi".
866882
Elpi Accumulate File "HB/common/utils.elpi".
@@ -895,6 +911,7 @@ Elpi Export HB.declare.
895911

896912
#[arguments(raw)] Elpi Command HB.check.
897913
Elpi Accumulate Db hb.db.
914+
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
898915
Elpi Accumulate File "HB/common/stdpp.elpi".
899916
Elpi Accumulate File "HB/common/database.elpi".
900917
Elpi Accumulate File "HB/common/utils.elpi".

0 commit comments

Comments
 (0)