-
Notifications
You must be signed in to change notification settings - Fork 43
/
_HoTTProject
75 lines (68 loc) · 1.47 KB
/
_HoTTProject
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
-I src
-I test-suite
-Q theories Equations
-Q src Equations
-I theories
-I examples
COQFLAGS = "-noinit -indices-matter"
CAMLDEBUG = "-bin-annot -g -for-pack Equations -w -58"
COQDOCFLAGS = "-parse-comments -utf8 -interpolate"
src/equations_common.mli
src/equations_common.ml
src/ederive.ml
src/ederive.mli
src/sigma_types.mli
src/sigma_types.ml
src/subterm.mli
src/subterm.ml
src/eqdec.mli
src/eqdec.ml
src/depelim.mli
src/depelim.ml
src/syntax.mli
src/syntax.ml
src/context_map.mli
src/context_map.ml
src/simplify.mli
src/simplify.ml
src/splitting.mli
src/splitting.ml
src/covering.mli
src/covering.ml
src/principles_proofs.mli
src/principles_proofs.ml
src/principles.mli
src/principles.ml
src/equations.mli
src/equations.ml
src/noconf.ml
src/noconf.mli
src/noconf_hom.ml
src/noconf_hom.mli
src/extra_tactics.ml
src/extra_tactics.mli
src/g_equations.mlg
src/equations_plugin.mllib
theories/Init.v
theories/Signature.v
theories/CoreTactics.v
# HoTT-specific files needing the HoTT library.
theories/HoTT/Logic.v
theories/HoTT/Relation.v
theories/HoTT/Relation_Properties.v
theories/HoTT/WellFounded.v
theories/HoTT/Classes.v
theories/HoTT/EqDec.v
theories/HoTT/DepElim.v
theories/HoTT/FunctionalInduction.v
theories/HoTT/Constants.v
theories/HoTT/Tactics.v
theories/HoTT/Subterm.v
theories/HoTT/NoConfusion.v
theories/HoTT/EqDecInstances.v
theories/HoTT/Loader.v
theories/HoTT/Telescopes.v
theories/HoTT/WellFoundedInstances.v
theories/HoTT/All.v
test-suite/BasicsHoTT.v
test-suite/issues/issue389.v