-
Notifications
You must be signed in to change notification settings - Fork 5
/
Copy path_CoqProject
92 lines (75 loc) · 3.55 KB
/
_CoqProject
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
-I src
-I src/usability
-I src/components/abstraction
-I src/automation
-I src/coq-plugin-lib/src/utilities
-I src/coq-plugin-lib/src/coq
-I src/coq-plugin-lib/src/coq/constants
-I src/coq-plugin-lib/src/coq/termutils
-I src/coq-plugin-lib/src/coq/representationutils
-I src/coq-plugin-lib/src/coq/logicutils
-I src/coq-plugin-lib/src/coq/logicutils/hofs
-I src/coq-plugin-lib/src/coq/logicutils/contexts
-I src/coq-plugin-lib/src/coq/logicutils/inductive
-I src/coq-plugin-lib/src/coq/logicutils/transformation
-I src/coq-plugin-lib/src/coq/logicutils/typesandequality
-I src/coq-plugin-lib/src/coq/devutils
-R src Fixtranslation
-Q theories Fixtranslation
src/coq-plugin-lib/src/utilities/utilities.mli
src/coq-plugin-lib/src/utilities/utilities.ml
src/coq-plugin-lib/src/coq/termutils/apputils.mli
src/coq-plugin-lib/src/coq/termutils/apputils.ml
src/coq-plugin-lib/src/coq/termutils/funutils.mli
src/coq-plugin-lib/src/coq/termutils/funutils.ml
src/coq-plugin-lib/src/coq/representationutils/defutils.mli
src/coq-plugin-lib/src/coq/representationutils/defutils.ml
src/coq-plugin-lib/src/coq/representationutils/nameutils.mli
src/coq-plugin-lib/src/coq/representationutils/nameutils.ml
src/coq-plugin-lib/src/coq/logicutils/typesandequality/inference.mli
src/coq-plugin-lib/src/coq/logicutils/typesandequality/inference.ml
src/coq-plugin-lib/src/coq/logicutils/typesandequality/convertibility.mli
src/coq-plugin-lib/src/coq/logicutils/typesandequality/convertibility.ml
src/coq-plugin-lib/src/coq/logicutils/typesandequality/checking.mli
src/coq-plugin-lib/src/coq/logicutils/typesandequality/checking.ml
src/coq-plugin-lib/src/coq/constants/idutils.mli
src/coq-plugin-lib/src/coq/constants/idutils.ml
src/coq-plugin-lib/src/coq/constants/sigmautils.mli
src/coq-plugin-lib/src/coq/constants/sigmautils.ml
src/coq-plugin-lib/src/coq/logicutils/contexts/stateutils.mli
src/coq-plugin-lib/src/coq/logicutils/contexts/stateutils.ml
src/coq-plugin-lib/src/coq/logicutils/contexts/envutils.mli
src/coq-plugin-lib/src/coq/logicutils/contexts/envutils.ml
src/coq-plugin-lib/src/coq/logicutils/contexts/contextutils.mli
src/coq-plugin-lib/src/coq/logicutils/contexts/contextutils.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/hofs.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/debruijn.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/debruijn.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/substitution.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/substitution.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/reducers.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/reducers.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/zooming.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/zooming.ml
src/coq-plugin-lib/src/coq/logicutils/hofs/filters.mli
src/coq-plugin-lib/src/coq/logicutils/hofs/filters.ml
src/coq-plugin-lib/src/coq/logicutils/inductive/indutils.mli
src/coq-plugin-lib/src/coq/logicutils/inductive/indutils.ml
src/coq-plugin-lib/src/coq/logicutils/contexts/modutils.mli
src/coq-plugin-lib/src/coq/logicutils/contexts/modutils.ml
src/coq-plugin-lib/src/coq/logicutils/transformation/transform.mli
src/coq-plugin-lib/src/coq/logicutils/transformation/transform.ml
src/coq-plugin-lib/src/coq/devutils/printing.mli
src/coq-plugin-lib/src/coq/devutils/printing.ml
src/usability/preprocess_errors.mli
src/usability/preprocess_errors.ml
src/components/abstraction/abstraction.mli
src/components/abstraction/abstraction.ml
src/automation/desugar.mli
src/automation/desugar.ml
src/options.mli
src/options.ml
src/fixtranslation.ml4
src/fixtoelim.mlpack
theories/Fixtoelim.v