1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
|
# Search paths for all packages. They must all match the regex
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q stdpp stdpp
-Q stdpp_bitvector stdpp.bitvector
-Q stdpp_unstable stdpp.unstable
# Custom flags (to be kept in sync with the dune file at the root of the repo).
# Fixing this one requires Coq 8.19
-arg -w -arg -argument-scope-delimiter
# Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -notation-incompatible-prefix
# We can't do this migration yet until we require Coq 9.0
-arg -w -arg -deprecated-from-Coq
-arg -w -arg -deprecated-dirpath-Coq
stdpp/options.v
stdpp/base.v
stdpp/tactics.v
stdpp/option.v
stdpp/fin_map_dom.v
stdpp/boolset.v
stdpp/fin_maps.v
stdpp/fin.v
stdpp/vector.v
stdpp/pmap.v
stdpp/stringmap.v
stdpp/fin_sets.v
stdpp/mapset.v
stdpp/proof_irrel.v
stdpp/hashset.v
stdpp/pretty.v
stdpp/countable.v
stdpp/orders.v
stdpp/natmap.v
stdpp/strings.v
stdpp/well_founded.v
stdpp/relations.v
stdpp/sets.v
stdpp/listset.v
stdpp/streams.v
stdpp/gmap.v
stdpp/gmultiset.v
stdpp/prelude.v
stdpp/listset_nodup.v
stdpp/finite.v
stdpp/numbers.v
stdpp/nmap.v
stdpp/zmap.v
stdpp/coPset.v
stdpp/coGset.v
stdpp/lexico.v
stdpp/propset.v
stdpp/decidable.v
stdpp/list.v
stdpp/list_numbers.v
stdpp/functions.v
stdpp/hlist.v
stdpp/sorting.v
stdpp/infinite.v
stdpp/nat_cancel.v
stdpp/namespaces.v
stdpp/telescopes.v
stdpp/binders.v
stdpp/ssreflect.v
stdpp_bitvector/definitions.v
stdpp_bitvector/tactics.v
stdpp_bitvector/bitvector.v
stdpp_unstable/bitblast.v
|
