Skip to content

Commit 5b2ca8a

Browse files
proux01proux01
committed
Compat Coq 8.15
1 parent c6d0dd6 commit 5b2ca8a

File tree

4 files changed

+22
-2
lines changed

4 files changed

+22
-2
lines changed

‎HB/common/compat_815.elpi‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1,2 @@
1-
macro @reversible! :- true.
1+
pred compat.coercion.declare i:coercion.
2+
compat.coercion.declare C :- @global! => coq.coercion.declare C.

‎HB/common/compat_all.elpi‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
pred compat.coercion.declare i:coercion.
2+
compat.coercion.declare C :- @global! => @reversible! => coq.coercion.declare C.

‎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-
@global! => @reversible! => coq.coercion.declare C,
162+
compat.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),

‎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+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
251252
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
252253
Elpi Accumulate lp:{{
253254

@@ -278,6 +279,7 @@ Elpi Export HB.locate.
278279
*)
279280

280281
#[arguments(raw)] Elpi Command HB.about.
282+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
281283
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
282284
Elpi Accumulate File "HB/common/stdpp.elpi".
283285
Elpi Accumulate File "HB/common/database.elpi".
@@ -304,6 +306,7 @@ Elpi Export HB.about.
304306
*)
305307

306308
#[arguments(raw)] Elpi Command HB.status.
309+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
307310
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
308311
Elpi Accumulate File "HB/common/stdpp.elpi".
309312
Elpi Accumulate File "HB/common/database.elpi".
@@ -331,6 +334,7 @@ tred file.dot | xdot -
331334
*)
332335

333336
#[arguments(raw)] Elpi Command HB.graph.
337+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
334338
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
335339
Elpi Accumulate File "HB/common/stdpp.elpi".
336340
Elpi Accumulate File "HB/common/database.elpi".
@@ -378,6 +382,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
378382
*)
379383

380384
#[arguments(raw)] Elpi Command HB.mixin.
385+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
381386
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
382387
Elpi Accumulate File "HB/common/stdpp.elpi".
383388
Elpi Accumulate File "HB/common/database.elpi".
@@ -439,6 +444,7 @@ Elpi Export HB.mixin.
439444

440445
Elpi Tactic HB.pack_for.
441446
Elpi Accumulate Db hb.db.
447+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
442448
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
443449
Elpi Accumulate File "HB/common/stdpp.elpi".
444450
Elpi Accumulate File "HB/common/database.elpi".
@@ -460,6 +466,7 @@ Elpi Export HB.pack_for.
460466

461467
Elpi Tactic HB.pack.
462468
Elpi Accumulate Db hb.db.
469+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
463470
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
464471
Elpi Accumulate File "HB/common/stdpp.elpi".
465472
Elpi Accumulate File "HB/common/database.elpi".
@@ -542,6 +549,7 @@ HB.structure Definition StructureName params :=
542549
*)
543550

544551
#[arguments(raw)] Elpi Command HB.structure.
552+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
545553
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
546554
Elpi Accumulate File "HB/common/stdpp.elpi".
547555
Elpi Accumulate File "HB/common/database.elpi".
@@ -595,6 +603,7 @@ HB.instance Definition N Params := Factory.Build Params T …
595603
*)
596604

597605
#[arguments(raw)] Elpi Command HB.instance.
606+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
598607
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
599608
Elpi Accumulate File "HB/common/stdpp.elpi".
600609
Elpi Accumulate File "HB/common/database.elpi".
@@ -625,6 +634,7 @@ Elpi Export HB.instance.
625634
(** [HB.factory] declares a factory. It has the same syntax of [HB.mixin] *)
626635

627636
#[arguments(raw)] Elpi Command HB.factory.
637+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
628638
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
629639
Elpi Accumulate File "HB/common/stdpp.elpi".
630640
Elpi Accumulate File "HB/common/database.elpi".
@@ -684,6 +694,7 @@ HB.end.
684694
*)
685695

686696
#[arguments(raw)] Elpi Command HB.builders.
697+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
687698
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
688699
Elpi Accumulate File "HB/common/stdpp.elpi".
689700
Elpi Accumulate File "HB/common/database.elpi".
@@ -707,6 +718,7 @@ Elpi Export HB.builders.
707718

708719

709720
#[arguments(raw)] Elpi Command HB.end.
721+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
710722
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
711723
Elpi Accumulate File "HB/common/stdpp.elpi".
712724
Elpi Accumulate File "HB/common/database.elpi".
@@ -758,6 +770,7 @@ Export Algebra.Exports.
758770
*)
759771

760772
#[arguments(raw)] Elpi Command HB.export.
773+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
761774
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
762775
Elpi Accumulate File "HB/common/stdpp.elpi".
763776
Elpi Accumulate File "HB/common/database.elpi".
@@ -783,6 +796,7 @@ Elpi Export HB.export.
783796
(a module which is not closed yet) *)
784797

785798
#[arguments(raw)] Elpi Command HB.reexport.
799+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
786800
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
787801
Elpi Accumulate File "HB/common/stdpp.elpi".
788802
Elpi Accumulate File "HB/common/database.elpi".
@@ -828,6 +842,7 @@ Notation foo := foo.body.
828842
*)
829843

830844
#[arguments(raw)] Elpi Command HB.lock.
845+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
831846
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
832847
Elpi Accumulate File "HB/common/stdpp.elpi".
833848
Elpi Accumulate File "HB/common/database.elpi".
@@ -876,6 +891,7 @@ HB.instance Definition _ : Ml ... T := ml.
876891
*)
877892

878893
#[arguments(raw)] Elpi Command HB.declare.
894+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
879895
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
880896
Elpi Accumulate File "HB/common/stdpp.elpi".
881897
Elpi Accumulate File "HB/common/database.elpi".
@@ -911,6 +927,7 @@ Elpi Export HB.declare.
911927

912928
#[arguments(raw)] Elpi Command HB.check.
913929
Elpi Accumulate Db hb.db.
930+
#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
914931
#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
915932
Elpi Accumulate File "HB/common/stdpp.elpi".
916933
Elpi Accumulate File "HB/common/database.elpi".

0 commit comments

Comments
 (0)