Skip to content

Commit 9e81748

Browse files
proux01proux01
committed
Compile without Stdlib
1 parent 7cbf30d commit 9e81748

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

66 files changed

+215
-150
lines changed

‎.github/workflows/main.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ jobs:
2121
- '8.18'
2222
- '8.19'
2323
- '8.20'
24+
- '9.0'
2425
steps:
2526
- uses: actions/checkout@v2
2627
- uses: coq-community/docker-coq-action@v1

‎Changelog.md

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,10 @@
11
# Changelog
22

3+
## Unreleased
4+
5+
Compile without coqc compatibility shim on Rocq 9.0
6+
Compile without Stdlb on Rocq 9.0
7+
38
## [1.8.1] - 2025-01-25
49

510
Compatible with

‎HB/common/compat_acc_clauses_816.elpi

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

‎HB/structures.v

Lines changed: 18 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
(* Support constants, to be kept in sync with shim/structures.v *)
2-
From Coq Require Import String ssreflect ssrfun.
3-
Export String.StringSyntax.
2+
From Corelib Require Import ssreflect ssrfun.
43

54
Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
65
Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
@@ -300,8 +299,7 @@ Elpi Accumulate Db hb.db.
300299
Elpi Accumulate File "HB/common/stdpp.elpi".
301300
Elpi Accumulate File "HB/common/utils.elpi".
302301
Elpi Accumulate File "HB/common/database.elpi".
303-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
304-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
302+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
305303
Elpi Accumulate File "HB/common/log.elpi".
306304
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
307305
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
@@ -335,8 +333,7 @@ Elpi Export HB.about.
335333
Elpi Accumulate Db hb.db.
336334
Elpi Accumulate File "HB/common/stdpp.elpi".
337335
Elpi Accumulate File "HB/common/database.elpi".
338-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
339-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
336+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
340337
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
341338
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
342339
Elpi Accumulate File "HB/common/utils.elpi".
@@ -379,8 +376,7 @@ Elpi Export HB.howto.
379376
Elpi Accumulate Db hb.db.
380377
Elpi Accumulate File "HB/common/stdpp.elpi".
381378
Elpi Accumulate File "HB/common/database.elpi".
382-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
383-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
379+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
384380
Elpi Accumulate File "HB/common/log.elpi".
385381
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
386382
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
@@ -411,8 +407,7 @@ tred file.dot | xdot -
411407
Elpi Accumulate Db hb.db.
412408
Elpi Accumulate File "HB/common/stdpp.elpi".
413409
Elpi Accumulate File "HB/common/database.elpi".
414-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
415-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
410+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
416411
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
417412
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
418413
Elpi Accumulate File "HB/common/utils.elpi".
@@ -462,8 +457,7 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
462457
Elpi Accumulate Db hb.db.
463458
Elpi Accumulate File "HB/common/stdpp.elpi".
464459
Elpi Accumulate File "HB/common/database.elpi".
465-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
466-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
460+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
467461
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
468462
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
469463
Elpi Accumulate File "HB/common/utils.elpi".
@@ -546,8 +540,7 @@ Elpi Tactic HB.pack_for.
546540
Elpi Accumulate Db hb.db.
547541
Elpi Accumulate File "HB/common/stdpp.elpi".
548542
Elpi Accumulate File "HB/common/database.elpi".
549-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
550-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
543+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
551544
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
552545
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
553546
Elpi Accumulate File "HB/common/utils.elpi".
@@ -571,8 +564,7 @@ Elpi Tactic HB.pack.
571564
Elpi Accumulate Db hb.db.
572565
Elpi Accumulate File "HB/common/stdpp.elpi".
573566
Elpi Accumulate File "HB/common/database.elpi".
574-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
575-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
567+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
576568
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
577569
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
578570
Elpi Accumulate File "HB/common/utils.elpi".
@@ -649,8 +641,7 @@ HB.structure Definition StructureName params :=
649641
Elpi Accumulate Db hb.db.
650642
Elpi Accumulate File "HB/common/stdpp.elpi".
651643
Elpi Accumulate File "HB/common/database.elpi".
652-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
653-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
644+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
654645
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
655646
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
656647
Elpi Accumulate File "HB/common/utils.elpi".
@@ -734,8 +725,7 @@ Elpi Export HB.structure.
734725
Elpi Accumulate Db hb.db.
735726
Elpi Accumulate File "HB/common/stdpp.elpi".
736727
Elpi Accumulate File "HB/common/database.elpi".
737-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
738-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
728+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
739729
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
740730
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
741731
Elpi Accumulate File "HB/common/utils.elpi".
@@ -786,8 +776,7 @@ HB.instance Definition N Params := Factory.Build Params T …
786776
Elpi Accumulate Db hb.db.
787777
Elpi Accumulate File "HB/common/stdpp.elpi".
788778
Elpi Accumulate File "HB/common/database.elpi".
789-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
790-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
779+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
791780
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
792781
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
793782
Elpi Accumulate File "HB/common/utils.elpi".
@@ -830,8 +819,7 @@ Elpi Export HB.instance.
830819
Elpi Accumulate Db hb.db.
831820
Elpi Accumulate File "HB/common/stdpp.elpi".
832821
Elpi Accumulate File "HB/common/database.elpi".
833-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
834-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
822+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
835823
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
836824
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
837825
Elpi Accumulate File "HB/common/utils.elpi".
@@ -915,8 +903,7 @@ HB.end.
915903
Elpi Accumulate Db hb.db.
916904
Elpi Accumulate File "HB/common/stdpp.elpi".
917905
Elpi Accumulate File "HB/common/database.elpi".
918-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
919-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
906+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
920907
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
921908
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
922909
Elpi Accumulate File "HB/common/utils.elpi".
@@ -958,8 +945,7 @@ Elpi Export HB.builders.
958945
Elpi Accumulate Db hb.db.
959946
Elpi Accumulate File "HB/common/stdpp.elpi".
960947
Elpi Accumulate File "HB/common/database.elpi".
961-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
962-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
948+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
963949
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
964950
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
965951
Elpi Accumulate File "HB/common/utils.elpi".
@@ -1034,8 +1020,7 @@ Export Algebra.Exports.
10341020
Elpi Accumulate Db hb.db.
10351021
Elpi Accumulate File "HB/common/stdpp.elpi".
10361022
Elpi Accumulate File "HB/common/database.elpi".
1037-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1038-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1023+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
10391024
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
10401025
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
10411026
Elpi Accumulate File "HB/common/utils.elpi".
@@ -1082,8 +1067,7 @@ Elpi Export HB.export.
10821067
Elpi Accumulate Db hb.db.
10831068
Elpi Accumulate File "HB/common/stdpp.elpi".
10841069
Elpi Accumulate File "HB/common/database.elpi".
1085-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1086-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1070+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
10871071
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
10881072
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
10891073
Elpi Accumulate File "HB/common/utils.elpi".
@@ -1167,8 +1151,7 @@ HB.instance Definition _ : Ml ... T := ml.
11671151
Elpi Accumulate Db hb.db.
11681152
Elpi Accumulate File "HB/common/stdpp.elpi".
11691153
Elpi Accumulate File "HB/common/database.elpi".
1170-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1171-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1154+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
11721155
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
11731156
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
11741157
Elpi Accumulate File "HB/common/utils.elpi".
@@ -1205,8 +1188,7 @@ Elpi Export HB.declare.
12051188
Elpi Accumulate Db hb.db.
12061189
Elpi Accumulate File "HB/common/stdpp.elpi".
12071190
Elpi Accumulate File "HB/common/database.elpi".
1208-
#[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
1209-
#[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
1191+
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
12101192
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
12111193
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
12121194
Elpi Accumulate File "HB/common/utils.elpi".
@@ -1246,8 +1228,3 @@ Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None)
12461228
Notation "`Error: t `is_not_canonically_a T" := (unify t _ (Some (is_not_canonically_a, T)))
12471229
(at level 0, T at level 0, format "`Error: t `is_not_canonically_a T", only printing) :
12481230
form_scope.
1249-
Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T)))
1250-
(at level 0, msg, T at level 0, format "`Error: t msg T", only printing) :
1251-
form_scope.
1252-
1253-
Global Open Scope string_scope.

‎Makefile

Lines changed: 20 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,14 @@ TGTS?=
2626
######################################################################
2727

2828
# local context: -----------------------------------------------------
29-
.PHONY: all config build only test-suite clean distclean __always__
29+
.PHONY: all config build only test-suite test-suite-stdlib clean distclean __always__
3030
.SUFFIXES:
3131

3232
H:= $(if $(VERBOSE),,@) # not used yet
3333
TOP = $(dir $(lastword $(MAKEFILE_LIST)))
3434
COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
3535
COQMAKE_TESTSUITE = $(MAKE) -f Makefile.test-suite.coq $(COQMAKEOPTIONS)
36+
COQMAKE_TESTSUITE_STDLIB = $(MAKE) -f Makefile.test-suite-stdlib.coq $(COQMAKEOPTIONS)
3637
BRANCH_coq:= $(shell $(COQTOP) -v | head -1 | grep -E '(trunk|master)' \
3738
| wc -l | sed 's/ *//g')
3839

@@ -75,6 +76,11 @@ Makefile.coq: $(COQPROJECT) Makefile
7576
Makefile.test-suite.coq: $(COQPROJECT).test-suite Makefile
7677
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite -o Makefile.test-suite.coq
7778

79+
# Test suite Stdlib --------------------------------------------------
80+
81+
Makefile.test-suite-stdlib.coq: $(COQPROJECT).test-suite-stdlib Makefile
82+
$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT).test-suite-stdlib -o Makefile.test-suite-stdlib.coq
83+
7884
# Global config, build, clean and distclean --------------------------
7985
config: sub-config this-config
8086

@@ -84,14 +90,19 @@ only: sub-only this-only
8490

8591
test-suite: sub-test-suite this-test-suite
8692

93+
test-suite-stdlib: sub-test-suite-stdlib this-test-suite-stdlib
94+
8795
clean: sub-clean this-clean
8896

8997
distclean: sub-distclean this-distclean
9098

9199
# Local config, build, clean and distclean ---------------------------
92-
.PHONY: this-config this-build this-only this-test-suite this-distclean this-clean
100+
.PHONY: this-config this-build this-only this-test-suite this-test-suite-stdlib this-distclean this-clean
93101

94102
this-config:: __always__
103+
if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
104+
sed -i.bak HB/structures.v -e 's/From Corelib/From Coq/' ; \
105+
fi
95106

96107
this-build:: this-config Makefile.coq
97108
+$(COQMAKE)
@@ -102,13 +113,18 @@ this-only:: this-config Makefile.coq
102113
this-test-suite:: build Makefile.test-suite.coq
103114
+$(COQMAKE_TESTSUITE)
104115

116+
this-test-suite-stdlib:: build Makefile.test-suite-stdlib.coq
117+
+$(COQMAKE_TESTSUITE_STDLIB)
118+
105119
this-distclean:: this-clean
106120
rm -f Makefile.coq Makefile.coq.conf
107121
rm -f Makefile.test-suite.coq Makefile.test-suite.coq.conf
122+
rm -f Makefile.test-suite-stdlib.coq Makefile.test-suite-stdlib.coq.conf
108123

109124
this-clean:: __always__
110125
@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
111126
@if [ -f Makefile.test-suite.coq ]; then $(COQMAKE_TESTSUITE) cleanall; fi
127+
@if [ -f Makefile.test-suite-stdlib.coq ]; then $(COQMAKE_TESTSUITE_STDLIB) cleanall; fi
112128

113129
# Install target -----------------------------------------------------
114130
.PHONY: install
@@ -142,5 +158,6 @@ endif
142158
structures.vo : %.vo: __always__ Makefile.coq
143159
+$(COQMAKE) $@
144160

145-
$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq
161+
$(addsuffix o,$(wildcard examples/*.v examples/*/*.v tests/*.v tests/unit/*.v)): __always__ config build Makefile.test-suite.coq Makefile.test-suite-stdlib.coq
146162
+$(COQMAKE_TESTSUITE) $@
163+
+$(COQMAKE_TESTSUITE_stdlib) $@

‎Makefile.test-suite.coq.local

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,8 +23,6 @@ DIFF=\
2323
post-all::
2424
$(call DIFF, tests/err_missin_subject.v)
2525
$(call DIFF, tests/compress_coe.v)
26-
$(call DIFF, tests/about.v)
27-
$(call DIFF, tests/howto.v)
2826
$(call DIFF, tests/err_miss_key.v)
2927
$(call DIFF, tests/missing_join_error.v)
3028
$(call DIFF, tests/not_same_key.v)

‎_CoqProject.test-suite

Lines changed: 0 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -8,26 +8,6 @@
88
examples/readme.v
99
examples/hulk.v
1010

11-
examples/demo1/hierarchy_0.v
12-
examples/demo1/hierarchy_1.v
13-
examples/demo1/hierarchy_2.v
14-
examples/demo1/hierarchy_3.v
15-
examples/demo1/hierarchy_4.v
16-
examples/demo1/hierarchy_5.v
17-
examples/demo1/test_0_0.v
18-
examples/demo1/test_1_0.v
19-
examples/demo1/test_2_0.v
20-
examples/demo1/test_3_0.v
21-
examples/demo1/test_3_3.v
22-
examples/demo1/test_4_0.v
23-
examples/demo1/test_4_3.v
24-
examples/demo1/test_5_0.v
25-
examples/demo1/test_5_3.v
26-
27-
examples/demo2/classical.v
28-
examples/demo2/stage10.v
29-
examples/demo2/stage11.v
30-
3111
examples/demo3/hierarchy_0.v
3212
examples/demo3/hierarchy_1.v
3313
examples/demo3/hierarchy_2.v
@@ -39,32 +19,15 @@ examples/demo4/hierarchy_0.v
3919

4020
examples/demo5/hierarchy_0.v
4121

42-
examples/FSCD2020_material/V1.v
43-
examples/FSCD2020_material/V2.v
44-
examples/FSCD2020_material/V3.v
45-
examples/FSCD2020_material/V4.v
46-
47-
examples/FSCD2020_talk/V1.v
48-
examples/FSCD2020_talk/V2.v
49-
examples/FSCD2020_talk/V3.v
50-
51-
examples/Coq2020_material/CoqWS_demo.v
52-
examples/Coq2020_material/CoqWS_abstract.v
53-
examples/Coq2020_material/CoqWS_expansion/withHB.v
54-
examples/Coq2020_material/CoqWS_expansion/withoutHB.v
55-
5622
# examples/cat/cat.v
5723

5824
tests/type_of_exported_ops.v
5925
tests/duplicate_structure.v
6026
tests/instance_params_no_type.v
6127
tests/test_CS_db_filtering.v
6228
tests/subtype.v
63-
tests/exports.v
64-
tests/exports2.v
6529
tests/log_impargs_record.v
6630
tests/compress_coe.v
67-
tests/funclass.v
6831
tests/grefclass.v
6932
tests/local_instance.v
7033
tests/lock.v

0 commit comments

Comments
 (0)