forked from MetaRocq/metarocq
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path_CoqProject.in
119 lines (102 loc) · 3.1 KB
/
_CoqProject.in
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
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
-R theories MetaCoq.PCUIC
theories/PCUICAst.v
theories/PCUICMonadAst.v
theories/utils/PCUICOnOne.v
theories/utils/PCUICPrimitive.v
theories/utils/PCUICAstUtils.v
theories/utils/PCUICUtils.v
theories/utils/PCUICSize.v
theories/utils/PCUICPretty.v
theories/Syntax/PCUICCases.v
theories/Syntax/PCUICInduction.v
theories/Syntax/PCUICDepth.v
theories/Syntax/PCUICPosition.v
theories/Syntax/PCUICReflect.v
theories/Syntax/PCUICNamelessDef.v
theories/Syntax/PCUICOnFreeVars.v
theories/Syntax/PCUICRenameDef.v
theories/Syntax/PCUICInstDef.v
theories/Syntax/PCUICLiftSubst.v
theories/Syntax/PCUICTactics.v
theories/Syntax/PCUICUnivSubst.v
theories/Syntax/PCUICClosed.v
theories/Syntax/PCUICViews.v
theories/Conversion/PCUICNamelessConv.v
theories/Conversion/PCUICRenameConv.v
theories/Conversion/PCUICInstConv.v
theories/Conversion/PCUICWeakeningEnvConv.v
theories/Conversion/PCUICWeakeningConfigConv.v
theories/Conversion/PCUICUnivSubstitutionConv.v
theories/Conversion/PCUICWeakeningConv.v
theories/Conversion/PCUICClosedConv.v
theories/Conversion/PCUICOnFreeVarsConv.v
theories/Typing/PCUICNamelessTyp.v
theories/Typing/PCUICRenameTyp.v
theories/Typing/PCUICInstTyp.v
theories/Typing/PCUICWeakeningEnvTyp.v
theories/Typing/PCUICWeakeningConfigTyp.v
theories/Typing/PCUICWeakeningTyp.v
theories/Typing/PCUICUnivSubstitutionTyp.v
theories/Typing/PCUICClosedTyp.v
theories/Typing/PCUICContextConversionTyp.v
theories/PCUICContextSubst.v
theories/PCUICCasesContexts.v
theories/PCUICReduction.v
theories/PCUICTyping.v
theories/PCUICGuardCondition.v
theories/PCUICGlobalEnv.v
theories/PCUICInversion.v
theories/PCUICNormal.v
theories/PCUICEquality.v
theories/PCUICSubstitution.v
theories/PCUICContextReduction.v
theories/PCUICCumulativity.v
theories/PCUICCumulativitySpec.v
theories/PCUICParallelReduction.v
theories/PCUICParallelReductionConfluence.v
theories/PCUICConfluence.v
theories/PCUICWellScopedCumulativity.v
theories/PCUICContextConversion.v
theories/PCUICConversion.v
theories/PCUICConvCumInversion.v
theories/PCUICRedTypeIrrelevance.v
theories/PCUICGeneration.v
theories/PCUICAlpha.v
theories/PCUICContexts.v
theories/PCUICArities.v
theories/PCUICWfUniverses.v
theories/PCUICSpine.v
theories/PCUICInductives.v
theories/PCUICValidity.v
theories/PCUICInductiveInversion.v
theories/PCUICSR.v
theories/PCUICClassification.v
theories/PCUICCanonicity.v
theories/PCUICCSubst.v
theories/PCUICWcbvEval.v
theories/PCUICCumulProp.v
theories/PCUICElimination.v
theories/PCUICSN.v
theories/PCUICWeakeningEnvSN.v
theories/PCUICWeakeningConfigSN.v
theories/PCUICPrincipality.v
theories/PCUICSigmaCalculus.v
theories/PCUICFirstorder.v
theories/PCUICProgress.v
theories/PCUICNormalization.v
theories/PCUICConsistency.v
theories/PCUICSafeLemmata.v
theories/PCUICEtaExpand.v
theories/PCUICProgram.v
theories/PCUICExpandLets.v
theories/PCUICExpandLetsCorrectness.v
theories/Bidirectional/BDTyping.v
theories/Bidirectional/BDToPCUIC.v
theories/Bidirectional/BDFromPCUIC.v
theories/Bidirectional/BDUnique.v
theories/Bidirectional/BDStrengthening.v
theories/PCUICWeakeningEnv.v
theories/PCUICWeakeningConfig.v
theories/PCUICCasesHelper.v
theories/PCUICESubst.v
# theories/All.v