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
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
|
# Suppress harmless compiler warnings we can't do anything about.
-arg -w -arg -projection-no-head-constant
-arg -w -arg -notation-overridden
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -future-coercion-class-field
-R theories/ RelationAlgebra
-I src/
theories/common.v
theories/comparisons.v
theories/positives.v
theories/ordinal.v
theories/denum.v
theories/pair.v
theories/powerfix.v
theories/level.v
theories/lattice.v
theories/monoid.v
theories/kleene.v
theories/factors.v
theories/kat.v
theories/rewriting.v
theories/move.v
theories/lsyntax.v
theories/syntax.v
theories/normalisation.v
theories/prop.v
theories/boolean.v
theories/rel.v
theories/srel.v
theories/lang.v
theories/lset.v
theories/sups.v
theories/sums.v
theories/matrix.v
theories/matrix_ext.v
theories/untyping.v
theories/regex.v
theories/rmx.v
theories/bmx.v
theories/dfa.v
theories/nfa.v
theories/ka_completeness.v
theories/atoms.v
theories/traces.v
theories/glang.v
theories/gregex.v
theories/kat_completeness.v
theories/ugregex.v
theories/ugregex_dec.v
theories/kat_untyping.v
theories/kat_reification.v
theories/kat_tac.v
theories/relalg.v
theories/all.v
# examples of applications
examples/compiler_opts.v
examples/imp.v
examples/paterson.v
# plugin files
## shared utilities
src/common.ml
src/common.mli
src/plugins.mlpack
## the various plugins are packed separately: they don't load the same Coq refs
src/fold.ml
src/fold.mli
src/fold_g.mlg
src/fold_g.mli
src/packed_fold.mlpack
src/mrewrite.ml
src/mrewrite.mli
src/mrewrite_g.mlg
src/mrewrite_g.mli
src/packed_mrewrite.mlpack
src/reification.ml
src/reification.mli
src/reification_g.mlg
src/reification_g.mli
src/packed_reification.mlpack
src/kat_dec.ml
src/kat_dec.mli
src/kat_reification.ml
src/kat_reification.mli
src/kat_reification_g.mlg
src/kat_reification_g.mli
src/packed_kat.mlpack
src/META.coq-relation-algebra
# optional theory files are set below, via [configure] script
# theories/fhrel.v
# theories/rewriting_aac.v
|
