Skip to content

Commit 78fa343

Browse files
garesgares
committed
fix old coq
1 parent 3ffdfd3 commit 78fa343

File tree

4 files changed

+56
-13
lines changed

4 files changed

+56
-13
lines changed

‎HB/common/compat_add_secvar_18_19.elpi‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
pred log.coq.env.add-section-variable-noimplicits i:id, i:term, o:constant.
2+
log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [
3+
if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
4+
@local! => coq.env.add-section-variable ID Ty C,
5+
log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
6+
@local! => log.coq.arguments.set-implicit (const C) [[]],
7+
].
8+

‎HB/common/compat_add_secvar_all.elpi‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
pred log.coq.env.add-section-variable-noimplicits i:id, i:term, o:constant.
2+
log.coq.env.add-section-variable-noimplicits Name Ty C :- std.do! [
3+
if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
4+
% elpi:if version coq-elpi < 2.4.0
5+
@local! => coq.env.add-section-variable ID Ty C,
6+
% elpi:endif
7+
% elpi:if version coq-elpi >= 2.4.0
8+
@local! => coq.env.add-section-variable ID _ Ty C,
9+
% elpi:endif
10+
log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
11+
@local! => log.coq.arguments.set-implicit (const C) [[]],
12+
].
13+

‎HB/common/log.elpi‎

Lines changed: 0 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -68,19 +68,6 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [
6868
@local! => arguments.set-implicit (const C) [[]],
6969
].
7070

71-
pred env.add-section-variable-noimplicits i:id, i:term, o:constant.
72-
env.add-section-variable-noimplicits Name Ty C :- std.do! [
73-
if (Name = "_") (ID is "fresh_name_" ^ {std.any->string {new_int}}) (ID = Name),
74-
% elpi:if version coq-elpi < 2.4.0
75-
@local! => coq.env.add-section-variable ID Ty C,
76-
% elpi:endif
77-
% elpi:if version coq-elpi >= 2.4.0
78-
@local! => coq.env.add-section-variable ID _ Ty C,
79-
% elpi:endif
80-
log.private.log-vernac (log.private.coq.vernac.variable ID Ty),
81-
@local! => arguments.set-implicit (const C) [[]],
82-
].
83-
8471
pred env.add-parameter i:id, i:term, o:constant.
8572
env.add-parameter ID Ty C :- std.do! [
8673
@global! => coq.env.add-axiom ID Ty C,

‎HB/structures.v‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -303,6 +303,8 @@ Elpi Accumulate File "HB/common/database.elpi".
303303
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
304304
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
305305
Elpi Accumulate File "HB/common/log.elpi".
306+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
307+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
306308
Elpi Accumulate File "HB/about.elpi".
307309
Elpi Accumulate lp:{{
308310

@@ -335,6 +337,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
335337
Elpi Accumulate File "HB/common/database.elpi".
336338
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
337339
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
340+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
341+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
338342
Elpi Accumulate File "HB/common/utils.elpi".
339343
Elpi Accumulate File "HB/common/log.elpi".
340344
Elpi Accumulate File "HB/about.elpi".
@@ -377,6 +381,9 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
377381
Elpi Accumulate File "HB/common/database.elpi".
378382
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
379383
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
384+
Elpi Accumulate File "HB/common/log.elpi".
385+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
386+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
380387
Elpi Accumulate File "HB/common/utils.elpi".
381388
Elpi Accumulate File "HB/status.elpi".
382389
Elpi Accumulate lp:{{
@@ -406,6 +413,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
406413
Elpi Accumulate File "HB/common/database.elpi".
407414
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
408415
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
416+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
417+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
409418
Elpi Accumulate File "HB/common/utils.elpi".
410419
Elpi Accumulate File "HB/common/log.elpi".
411420
Elpi Accumulate File "HB/graph.elpi".
@@ -455,6 +464,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
455464
Elpi Accumulate File "HB/common/database.elpi".
456465
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
457466
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
467+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
468+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
458469
Elpi Accumulate File "HB/common/utils.elpi".
459470
Elpi Accumulate File "HB/common/log.elpi".
460471
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -537,6 +548,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
537548
Elpi Accumulate File "HB/common/database.elpi".
538549
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
539550
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
551+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
552+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
540553
Elpi Accumulate File "HB/common/utils.elpi".
541554
Elpi Accumulate File "HB/common/log.elpi".
542555
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -560,6 +573,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
560573
Elpi Accumulate File "HB/common/database.elpi".
561574
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
562575
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
576+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
577+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
563578
Elpi Accumulate File "HB/common/utils.elpi".
564579
Elpi Accumulate File "HB/common/log.elpi".
565580
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -636,6 +651,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
636651
Elpi Accumulate File "HB/common/database.elpi".
637652
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
638653
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
654+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
655+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
639656
Elpi Accumulate File "HB/common/utils.elpi".
640657
Elpi Accumulate File "HB/common/log.elpi".
641658
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -719,6 +736,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
719736
Elpi Accumulate File "HB/common/database.elpi".
720737
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
721738
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
739+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
740+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
722741
Elpi Accumulate File "HB/common/utils.elpi".
723742
Elpi Accumulate File "HB/common/log.elpi".
724743
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -769,6 +788,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
769788
Elpi Accumulate File "HB/common/database.elpi".
770789
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
771790
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
791+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
792+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
772793
Elpi Accumulate File "HB/common/utils.elpi".
773794
Elpi Accumulate File "HB/common/log.elpi".
774795
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -811,6 +832,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
811832
Elpi Accumulate File "HB/common/database.elpi".
812833
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
813834
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
835+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
836+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
814837
Elpi Accumulate File "HB/common/utils.elpi".
815838
Elpi Accumulate File "HB/common/log.elpi".
816839
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -894,6 +917,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
894917
Elpi Accumulate File "HB/common/database.elpi".
895918
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
896919
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
920+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
921+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
897922
Elpi Accumulate File "HB/common/utils.elpi".
898923
Elpi Accumulate File "HB/common/log.elpi".
899924
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -935,6 +960,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
935960
Elpi Accumulate File "HB/common/database.elpi".
936961
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
937962
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
963+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
964+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
938965
Elpi Accumulate File "HB/common/utils.elpi".
939966
Elpi Accumulate File "HB/common/log.elpi".
940967
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -1009,6 +1036,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
10091036
Elpi Accumulate File "HB/common/database.elpi".
10101037
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
10111038
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1039+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1040+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
10121041
Elpi Accumulate File "HB/common/utils.elpi".
10131042
Elpi Accumulate File "HB/common/log.elpi".
10141043
Elpi Accumulate File "HB/export.elpi".
@@ -1055,6 +1084,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
10551084
Elpi Accumulate File "HB/common/database.elpi".
10561085
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
10571086
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1087+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1088+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
10581089
Elpi Accumulate File "HB/common/utils.elpi".
10591090
Elpi Accumulate File "HB/common/log.elpi".
10601091
Elpi Accumulate File "HB/export.elpi".
@@ -1138,6 +1169,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
11381169
Elpi Accumulate File "HB/common/database.elpi".
11391170
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
11401171
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1172+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1173+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
11411174
Elpi Accumulate File "HB/common/utils.elpi".
11421175
Elpi Accumulate File "HB/common/log.elpi".
11431176
Elpi Accumulate File "HB/common/synthesis.elpi".
@@ -1174,6 +1207,8 @@ Elpi Accumulate File "HB/common/stdpp.elpi".
11741207
Elpi Accumulate File "HB/common/database.elpi".
11751208
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
11761209
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1210+
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
1211+
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
11771212
Elpi Accumulate File "HB/common/utils.elpi".
11781213
Elpi Accumulate File "HB/common/log.elpi".
11791214
Elpi Accumulate lp:{{

0 commit comments

Comments
 (0)