forked from peterlefanulumsdaine/general-type-theories
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy path.CoqMakefile.d
105 lines (105 loc) · 40.4 KB
/
.CoqMakefile.d
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
GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/General.glob GeneralTT/Auxiliary/General.v.beautified GeneralTT/Auxiliary/General.required_vo: GeneralTT/Auxiliary/General.v
GeneralTT/Auxiliary/General.vio: GeneralTT/Auxiliary/General.v
GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/General.vok GeneralTT/Auxiliary/General.required_vos: GeneralTT/Auxiliary/General.v
GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Auxiliary/WellFounded.glob GeneralTT/Auxiliary/WellFounded.v.beautified GeneralTT/Auxiliary/WellFounded.required_vo: GeneralTT/Auxiliary/WellFounded.v
GeneralTT/Auxiliary/WellFounded.vio: GeneralTT/Auxiliary/WellFounded.v
GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Auxiliary/WellFounded.vok GeneralTT/Auxiliary/WellFounded.required_vos: GeneralTT/Auxiliary/WellFounded.v
GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Family.glob GeneralTT/Auxiliary/Family.v.beautified GeneralTT/Auxiliary/Family.required_vo: GeneralTT/Auxiliary/Family.v
GeneralTT/Auxiliary/Family.vio: GeneralTT/Auxiliary/Family.v
GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Family.vok GeneralTT/Auxiliary/Family.required_vos: GeneralTT/Auxiliary/Family.v
GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Coproduct.glob GeneralTT/Auxiliary/Coproduct.v.beautified GeneralTT/Auxiliary/Coproduct.required_vo: GeneralTT/Auxiliary/Coproduct.v
GeneralTT/Auxiliary/Coproduct.vio: GeneralTT/Auxiliary/Coproduct.v
GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Coproduct.vok GeneralTT/Auxiliary/Coproduct.required_vos: GeneralTT/Auxiliary/Coproduct.v
GeneralTT/Auxiliary/Closure.vo GeneralTT/Auxiliary/Closure.glob GeneralTT/Auxiliary/Closure.v.beautified GeneralTT/Auxiliary/Closure.required_vo: GeneralTT/Auxiliary/Closure.v GeneralTT/Auxiliary/Family.vo
GeneralTT/Auxiliary/Closure.vio: GeneralTT/Auxiliary/Closure.v GeneralTT/Auxiliary/Family.vio
GeneralTT/Auxiliary/Closure.vos GeneralTT/Auxiliary/Closure.vok GeneralTT/Auxiliary/Closure.required_vos: GeneralTT/Auxiliary/Closure.v GeneralTT/Auxiliary/Family.vos
GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/ScopeSystem.glob GeneralTT/Syntax/ScopeSystem.v.beautified GeneralTT/Syntax/ScopeSystem.required_vo: GeneralTT/Syntax/ScopeSystem.v GeneralTT/Auxiliary/Coproduct.vo
GeneralTT/Syntax/ScopeSystem.vio: GeneralTT/Syntax/ScopeSystem.v GeneralTT/Auxiliary/Coproduct.vio
GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/ScopeSystem.vok GeneralTT/Syntax/ScopeSystem.required_vos: GeneralTT/Syntax/ScopeSystem.v GeneralTT/Auxiliary/Coproduct.vos
GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/SyntacticClass.glob GeneralTT/Syntax/SyntacticClass.v.beautified GeneralTT/Syntax/SyntacticClass.required_vo: GeneralTT/Syntax/SyntacticClass.v
GeneralTT/Syntax/SyntacticClass.vio: GeneralTT/Syntax/SyntacticClass.v
GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/SyntacticClass.vok GeneralTT/Syntax/SyntacticClass.required_vos: GeneralTT/Syntax/SyntacticClass.v
GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Arity.glob GeneralTT/Syntax/Arity.v.beautified GeneralTT/Syntax/Arity.required_vo: GeneralTT/Syntax/Arity.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Syntax/SyntacticClass.vo
GeneralTT/Syntax/Arity.vio: GeneralTT/Syntax/Arity.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Syntax/SyntacticClass.vio
GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Arity.vok GeneralTT/Syntax/Arity.required_vos: GeneralTT/Syntax/Arity.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Syntax/SyntacticClass.vos
GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/Signature.glob GeneralTT/Syntax/Signature.v.beautified GeneralTT/Syntax/Signature.required_vo: GeneralTT/Syntax/Signature.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Arity.vo
GeneralTT/Syntax/Signature.vio: GeneralTT/Syntax/Signature.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Arity.vio
GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/Signature.vok GeneralTT/Syntax/Signature.required_vos: GeneralTT/Syntax/Signature.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Arity.vos
GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Expression.glob GeneralTT/Syntax/Expression.v.beautified GeneralTT/Syntax/Expression.required_vo: GeneralTT/Syntax/Expression.v GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo
GeneralTT/Syntax/Expression.vio: GeneralTT/Syntax/Expression.v GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio
GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Expression.vok GeneralTT/Syntax/Expression.required_vos: GeneralTT/Syntax/Expression.v GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos
GeneralTT/Syntax/Substitution.vo GeneralTT/Syntax/Substitution.glob GeneralTT/Syntax/Substitution.v.beautified GeneralTT/Syntax/Substitution.required_vo: GeneralTT/Syntax/Substitution.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/Expression.vo
GeneralTT/Syntax/Substitution.vio: GeneralTT/Syntax/Substitution.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/Expression.vio
GeneralTT/Syntax/Substitution.vos GeneralTT/Syntax/Substitution.vok GeneralTT/Syntax/Substitution.required_vos: GeneralTT/Syntax/Substitution.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/Expression.vos
GeneralTT/Syntax/Metavariable.vo GeneralTT/Syntax/Metavariable.glob GeneralTT/Syntax/Metavariable.v.beautified GeneralTT/Syntax/Metavariable.required_vo: GeneralTT/Syntax/Metavariable.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Substitution.vo
GeneralTT/Syntax/Metavariable.vio: GeneralTT/Syntax/Metavariable.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/Expression.vio GeneralTT/Syntax/Substitution.vio
GeneralTT/Syntax/Metavariable.vos GeneralTT/Syntax/Metavariable.vok GeneralTT/Syntax/Metavariable.required_vos: GeneralTT/Syntax/Metavariable.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Substitution.vos
GeneralTT/Syntax/All.vo GeneralTT/Syntax/All.glob GeneralTT/Syntax/All.v.beautified GeneralTT/Syntax/All.required_vo: GeneralTT/Syntax/All.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Substitution.vo GeneralTT/Syntax/Metavariable.vo
GeneralTT/Syntax/All.vio: GeneralTT/Syntax/All.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/Expression.vio GeneralTT/Syntax/Substitution.vio GeneralTT/Syntax/Metavariable.vio
GeneralTT/Syntax/All.vos GeneralTT/Syntax/All.vok GeneralTT/Syntax/All.required_vos: GeneralTT/Syntax/All.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Substitution.vos GeneralTT/Syntax/Metavariable.vos
GeneralTT/Typing/Context.vo GeneralTT/Typing/Context.glob GeneralTT/Typing/Context.v.beautified GeneralTT/Typing/Context.required_vo: GeneralTT/Typing/Context.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Substitution.vo GeneralTT/Syntax/Metavariable.vo
GeneralTT/Typing/Context.vio: GeneralTT/Typing/Context.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/Expression.vio GeneralTT/Syntax/Substitution.vio GeneralTT/Syntax/Metavariable.vio
GeneralTT/Typing/Context.vos GeneralTT/Typing/Context.vok GeneralTT/Typing/Context.required_vos: GeneralTT/Typing/Context.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Substitution.vos GeneralTT/Syntax/Metavariable.vos
GeneralTT/Typing/Judgement.vo GeneralTT/Typing/Judgement.glob GeneralTT/Typing/Judgement.v.beautified GeneralTT/Typing/Judgement.required_vo: GeneralTT/Typing/Judgement.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Substitution.vo GeneralTT/Syntax/Metavariable.vo GeneralTT/Typing/Context.vo
GeneralTT/Typing/Judgement.vio: GeneralTT/Typing/Judgement.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Expression.vio GeneralTT/Syntax/Substitution.vio GeneralTT/Syntax/Metavariable.vio GeneralTT/Typing/Context.vio
GeneralTT/Typing/Judgement.vos GeneralTT/Typing/Judgement.vok GeneralTT/Typing/Judgement.required_vos: GeneralTT/Typing/Judgement.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Substitution.vos GeneralTT/Syntax/Metavariable.vos GeneralTT/Typing/Context.vos
GeneralTT/Typing/Presuppositions.vo GeneralTT/Typing/Presuppositions.glob GeneralTT/Typing/Presuppositions.v.beautified GeneralTT/Typing/Presuppositions.required_vo: GeneralTT/Typing/Presuppositions.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/Arity.vo GeneralTT/Syntax/Signature.vo GeneralTT/Syntax/SyntacticClass.vo GeneralTT/Syntax/Expression.vo GeneralTT/Syntax/Substitution.vo GeneralTT/Syntax/Metavariable.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawTypeTheory.vo
GeneralTT/Typing/Presuppositions.vio: GeneralTT/Typing/Presuppositions.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/Arity.vio GeneralTT/Syntax/Signature.vio GeneralTT/Syntax/SyntacticClass.vio GeneralTT/Syntax/Expression.vio GeneralTT/Syntax/Substitution.vio GeneralTT/Syntax/Metavariable.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/RawTypeTheory.vio
GeneralTT/Typing/Presuppositions.vos GeneralTT/Typing/Presuppositions.vok GeneralTT/Typing/Presuppositions.required_vos: GeneralTT/Typing/Presuppositions.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/Arity.vos GeneralTT/Syntax/Signature.vos GeneralTT/Syntax/SyntacticClass.vos GeneralTT/Syntax/Expression.vos GeneralTT/Syntax/Substitution.vos GeneralTT/Syntax/Metavariable.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawTypeTheory.vos
GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawRule.glob GeneralTT/Typing/RawRule.v.beautified GeneralTT/Typing/RawRule.required_vo: GeneralTT/Typing/RawRule.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Closure.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo
GeneralTT/Typing/RawRule.vio: GeneralTT/Typing/RawRule.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Closure.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio
GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawRule.vok GeneralTT/Typing/RawRule.required_vos: GeneralTT/Typing/RawRule.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Closure.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos
GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/StructuralRule.glob GeneralTT/Typing/StructuralRule.v.beautified GeneralTT/Typing/StructuralRule.required_vo: GeneralTT/Typing/StructuralRule.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Closure.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo
GeneralTT/Typing/StructuralRule.vio: GeneralTT/Typing/StructuralRule.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Closure.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio
GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/StructuralRule.vok GeneralTT/Typing/StructuralRule.required_vos: GeneralTT/Typing/StructuralRule.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Closure.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos
GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Typing/RawTypeTheory.glob GeneralTT/Typing/RawTypeTheory.v.beautified GeneralTT/Typing/RawTypeTheory.required_vo: GeneralTT/Typing/RawTypeTheory.v GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/StructuralRule.vo
GeneralTT/Typing/RawTypeTheory.vio: GeneralTT/Typing/RawTypeTheory.v GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/StructuralRule.vio
GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Typing/RawTypeTheory.vok GeneralTT/Typing/RawTypeTheory.required_vos: GeneralTT/Typing/RawTypeTheory.v GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/StructuralRule.vos
GeneralTT/Typing/StructuralRulePresuppositions.vo GeneralTT/Typing/StructuralRulePresuppositions.glob GeneralTT/Typing/StructuralRulePresuppositions.v.beautified GeneralTT/Typing/StructuralRulePresuppositions.required_vo: GeneralTT/Typing/StructuralRulePresuppositions.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/Presuppositions.vo
GeneralTT/Typing/StructuralRulePresuppositions.vio: GeneralTT/Typing/StructuralRulePresuppositions.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/Presuppositions.vio
GeneralTT/Typing/StructuralRulePresuppositions.vos GeneralTT/Typing/StructuralRulePresuppositions.vok GeneralTT/Typing/StructuralRulePresuppositions.required_vos: GeneralTT/Typing/StructuralRulePresuppositions.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/Presuppositions.vos
GeneralTT/Typing/All.vo GeneralTT/Typing/All.glob GeneralTT/Typing/All.v.beautified GeneralTT/Typing/All.required_vo: GeneralTT/Typing/All.v GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/Presuppositions.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Typing/StructuralRulePresuppositions.vo
GeneralTT/Typing/All.vio: GeneralTT/Typing/All.v GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/Presuppositions.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Typing/StructuralRulePresuppositions.vio
GeneralTT/Typing/All.vos GeneralTT/Typing/All.vok GeneralTT/Typing/All.required_vos: GeneralTT/Typing/All.v GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/Presuppositions.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Typing/StructuralRulePresuppositions.vos
GeneralTT/Presented/ContextVariants.vo GeneralTT/Presented/ContextVariants.glob GeneralTT/Presented/ContextVariants.v.beautified GeneralTT/Presented/ContextVariants.required_vo: GeneralTT/Presented/ContextVariants.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawTypeTheory.vo
GeneralTT/Presented/ContextVariants.vio: GeneralTT/Presented/ContextVariants.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/RawTypeTheory.vio
GeneralTT/Presented/ContextVariants.vos GeneralTT/Presented/ContextVariants.vok GeneralTT/Presented/ContextVariants.required_vos: GeneralTT/Presented/ContextVariants.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawTypeTheory.vos
GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Presented/AlgebraicExtension.glob GeneralTT/Presented/AlgebraicExtension.v.beautified GeneralTT/Presented/AlgebraicExtension.required_vo: GeneralTT/Presented/AlgebraicExtension.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo
GeneralTT/Presented/AlgebraicExtension.vio: GeneralTT/Presented/AlgebraicExtension.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio
GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Presented/AlgebraicExtension.vok GeneralTT/Presented/AlgebraicExtension.required_vos: GeneralTT/Presented/AlgebraicExtension.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos
GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawRule.glob GeneralTT/Presented/PresentedRawRule.v.beautified GeneralTT/Presented/PresentedRawRule.required_vo: GeneralTT/Presented/PresentedRawRule.v GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Closure.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Typing/RawRule.vo
GeneralTT/Presented/PresentedRawRule.vio: GeneralTT/Presented/PresentedRawRule.v GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Closure.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Presented/AlgebraicExtension.vio GeneralTT/Typing/RawRule.vio
GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawRule.vok GeneralTT/Presented/PresentedRawRule.required_vos: GeneralTT/Presented/PresentedRawRule.v GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Closure.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Typing/RawRule.vos
GeneralTT/Presented/CongruenceRule.vo GeneralTT/Presented/CongruenceRule.glob GeneralTT/Presented/CongruenceRule.v.beautified GeneralTT/Presented/CongruenceRule.required_vo: GeneralTT/Presented/CongruenceRule.v GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Presented/PresentedRawRule.vo
GeneralTT/Presented/CongruenceRule.vio: GeneralTT/Presented/CongruenceRule.v GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Presented/AlgebraicExtension.vio GeneralTT/Presented/PresentedRawRule.vio
GeneralTT/Presented/CongruenceRule.vos GeneralTT/Presented/CongruenceRule.vok GeneralTT/Presented/CongruenceRule.required_vos: GeneralTT/Presented/CongruenceRule.v GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Presented/PresentedRawRule.vos
GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Presented/PresentedRawTypeTheory.glob GeneralTT/Presented/PresentedRawTypeTheory.v.beautified GeneralTT/Presented/PresentedRawTypeTheory.required_vo: GeneralTT/Presented/PresentedRawTypeTheory.v GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Closure.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/CongruenceRule.vo
GeneralTT/Presented/PresentedRawTypeTheory.vio: GeneralTT/Presented/PresentedRawTypeTheory.v GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Closure.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/CongruenceRule.vio
GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Presented/PresentedRawTypeTheory.vok GeneralTT/Presented/PresentedRawTypeTheory.required_vos: GeneralTT/Presented/PresentedRawTypeTheory.v GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Closure.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/CongruenceRule.vos
GeneralTT/Presented/TypedRule.vo GeneralTT/Presented/TypedRule.glob GeneralTT/Presented/TypedRule.v.beautified GeneralTT/Presented/TypedRule.required_vo: GeneralTT/Presented/TypedRule.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Presented/CongruenceRule.vo GeneralTT/Typing/Presuppositions.vo
GeneralTT/Presented/TypedRule.vio: GeneralTT/Presented/TypedRule.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Presented/AlgebraicExtension.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/PresentedRawTypeTheory.vio GeneralTT/Presented/CongruenceRule.vio GeneralTT/Typing/Presuppositions.vio
GeneralTT/Presented/TypedRule.vos GeneralTT/Presented/TypedRule.vok GeneralTT/Presented/TypedRule.required_vos: GeneralTT/Presented/TypedRule.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Presented/CongruenceRule.vos GeneralTT/Typing/Presuppositions.vos
GeneralTT/Presented/TypeTheory.vo GeneralTT/Presented/TypeTheory.glob GeneralTT/Presented/TypeTheory.v.beautified GeneralTT/Presented/TypeTheory.required_vo: GeneralTT/Presented/TypeTheory.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Presented/TypedRule.vo
GeneralTT/Presented/TypeTheory.vio: GeneralTT/Presented/TypeTheory.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/PresentedRawTypeTheory.vio GeneralTT/Presented/TypedRule.vio
GeneralTT/Presented/TypeTheory.vos GeneralTT/Presented/TypeTheory.vok GeneralTT/Presented/TypeTheory.required_vos: GeneralTT/Presented/TypeTheory.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Presented/TypedRule.vos
GeneralTT/Metatheorem/UniqueTyping.vo GeneralTT/Metatheorem/UniqueTyping.glob GeneralTT/Metatheorem/UniqueTyping.v.beautified GeneralTT/Metatheorem/UniqueTyping.required_vo: GeneralTT/Metatheorem/UniqueTyping.v GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/All.vo GeneralTT/Presented/PresentedRawTypeTheory.vo
GeneralTT/Metatheorem/UniqueTyping.vio: GeneralTT/Metatheorem/UniqueTyping.v GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/All.vio GeneralTT/Presented/PresentedRawTypeTheory.vio
GeneralTT/Metatheorem/UniqueTyping.vos GeneralTT/Metatheorem/UniqueTyping.vok GeneralTT/Metatheorem/UniqueTyping.required_vos: GeneralTT/Metatheorem/UniqueTyping.v GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/All.vos GeneralTT/Presented/PresentedRawTypeTheory.vos
GeneralTT/Metatheorem/Elimination.vo GeneralTT/Metatheorem/Elimination.glob GeneralTT/Metatheorem/Elimination.v.beautified GeneralTT/Metatheorem/Elimination.required_vo: GeneralTT/Metatheorem/Elimination.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Closure.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/RawTypeTheory.vo
GeneralTT/Metatheorem/Elimination.vio: GeneralTT/Metatheorem/Elimination.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Closure.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/RawTypeTheory.vio
GeneralTT/Metatheorem/Elimination.vos GeneralTT/Metatheorem/Elimination.vok GeneralTT/Metatheorem/Elimination.required_vos: GeneralTT/Metatheorem/Elimination.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Closure.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/RawTypeTheory.vos
GeneralTT/Metatheorem/Presuppositions.vo GeneralTT/Metatheorem/Presuppositions.glob GeneralTT/Metatheorem/Presuppositions.v.beautified GeneralTT/Metatheorem/Presuppositions.required_vo: GeneralTT/Metatheorem/Presuppositions.v GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Auxiliary/General.vo GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Typing/Presuppositions.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Presented/CongruenceRule.vo GeneralTT/Typing/StructuralRulePresuppositions.vo GeneralTT/Presented/TypedRule.vo GeneralTT/Presented/TypeTheory.vo
GeneralTT/Metatheorem/Presuppositions.vio: GeneralTT/Metatheorem/Presuppositions.v GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Auxiliary/General.vio GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/PresentedRawTypeTheory.vio GeneralTT/Typing/Presuppositions.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Presented/CongruenceRule.vio GeneralTT/Typing/StructuralRulePresuppositions.vio GeneralTT/Presented/TypedRule.vio GeneralTT/Presented/TypeTheory.vio
GeneralTT/Metatheorem/Presuppositions.vos GeneralTT/Metatheorem/Presuppositions.vok GeneralTT/Metatheorem/Presuppositions.required_vos: GeneralTT/Metatheorem/Presuppositions.v GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Auxiliary/General.vos GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Typing/Presuppositions.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Presented/CongruenceRule.vos GeneralTT/Typing/StructuralRulePresuppositions.vos GeneralTT/Presented/TypedRule.vos GeneralTT/Presented/TypeTheory.vos
GeneralTT/Metatheorem/Acceptability.vo GeneralTT/Metatheorem/Acceptability.glob GeneralTT/Metatheorem/Acceptability.v.beautified GeneralTT/Metatheorem/Acceptability.required_vo: GeneralTT/Metatheorem/Acceptability.v GeneralTT/Syntax/All.vo GeneralTT/Typing/All.vo GeneralTT/Metatheorem/UniqueTyping.vo GeneralTT/Metatheorem/Elimination.vo GeneralTT/Metatheorem/Presuppositions.vo
GeneralTT/Metatheorem/Acceptability.vio: GeneralTT/Metatheorem/Acceptability.v GeneralTT/Syntax/All.vio GeneralTT/Typing/All.vio GeneralTT/Metatheorem/UniqueTyping.vio GeneralTT/Metatheorem/Elimination.vio GeneralTT/Metatheorem/Presuppositions.vio
GeneralTT/Metatheorem/Acceptability.vos GeneralTT/Metatheorem/Acceptability.vok GeneralTT/Metatheorem/Acceptability.required_vos: GeneralTT/Metatheorem/Acceptability.v GeneralTT/Syntax/All.vos GeneralTT/Typing/All.vos GeneralTT/Metatheorem/UniqueTyping.vos GeneralTT/Metatheorem/Elimination.vos GeneralTT/Metatheorem/Presuppositions.vos
GeneralTT/Example/ScopeSystemExamples.vo GeneralTT/Example/ScopeSystemExamples.glob GeneralTT/Example/ScopeSystemExamples.v.beautified GeneralTT/Example/ScopeSystemExamples.required_vo: GeneralTT/Example/ScopeSystemExamples.v GeneralTT/Syntax/All.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo
GeneralTT/Example/ScopeSystemExamples.vio: GeneralTT/Example/ScopeSystemExamples.v GeneralTT/Syntax/All.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio
GeneralTT/Example/ScopeSystemExamples.vos GeneralTT/Example/ScopeSystemExamples.vok GeneralTT/Example/ScopeSystemExamples.required_vos: GeneralTT/Example/ScopeSystemExamples.v GeneralTT/Syntax/All.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos
RegularCategories/DependentTypeTheory.vo RegularCategories/DependentTypeTheory.glob RegularCategories/DependentTypeTheory.v.beautified RegularCategories/DependentTypeTheory.required_vo: RegularCategories/DependentTypeTheory.v GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Presented/TypedRule.vo GeneralTT/Presented/TypeTheory.vo GeneralTT/Metatheorem/UniqueTyping.vo GeneralTT/Metatheorem/Elimination.vo GeneralTT/Metatheorem/Presuppositions.vo GeneralTT/Metatheorem/Acceptability.vo GeneralTT/Example/ScopeSystemExamples.vo
RegularCategories/DependentTypeTheory.vio: RegularCategories/DependentTypeTheory.v GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Presented/AlgebraicExtension.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/PresentedRawTypeTheory.vio GeneralTT/Presented/TypedRule.vio GeneralTT/Presented/TypeTheory.vio GeneralTT/Metatheorem/UniqueTyping.vio GeneralTT/Metatheorem/Elimination.vio GeneralTT/Metatheorem/Presuppositions.vio GeneralTT/Metatheorem/Acceptability.vio GeneralTT/Example/ScopeSystemExamples.vio
RegularCategories/DependentTypeTheory.vos RegularCategories/DependentTypeTheory.vok RegularCategories/DependentTypeTheory.required_vos: RegularCategories/DependentTypeTheory.v GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Presented/TypedRule.vos GeneralTT/Presented/TypeTheory.vos GeneralTT/Metatheorem/UniqueTyping.vos GeneralTT/Metatheorem/Elimination.vos GeneralTT/Metatheorem/Presuppositions.vos GeneralTT/Metatheorem/Acceptability.vos GeneralTT/Example/ScopeSystemExamples.vos
RegularCategories/Computability.vo RegularCategories/Computability.glob RegularCategories/Computability.v.beautified RegularCategories/Computability.required_vo: RegularCategories/Computability.v GeneralTT/Auxiliary/Family.vo GeneralTT/Auxiliary/Coproduct.vo GeneralTT/Syntax/ScopeSystem.vo GeneralTT/Syntax/All.vo GeneralTT/Typing/Context.vo GeneralTT/Typing/Judgement.vo GeneralTT/Typing/RawRule.vo GeneralTT/Typing/StructuralRule.vo GeneralTT/Typing/RawTypeTheory.vo GeneralTT/Auxiliary/WellFounded.vo GeneralTT/Presented/AlgebraicExtension.vo GeneralTT/Presented/PresentedRawRule.vo GeneralTT/Presented/PresentedRawTypeTheory.vo GeneralTT/Presented/TypedRule.vo GeneralTT/Presented/TypeTheory.vo GeneralTT/Metatheorem/UniqueTyping.vo GeneralTT/Metatheorem/Elimination.vo GeneralTT/Metatheorem/Presuppositions.vo GeneralTT/Metatheorem/Acceptability.vo GeneralTT/Example/ScopeSystemExamples.vo RegularCategories/DependentTypeTheory.vo
RegularCategories/Computability.vio: RegularCategories/Computability.v GeneralTT/Auxiliary/Family.vio GeneralTT/Auxiliary/Coproduct.vio GeneralTT/Syntax/ScopeSystem.vio GeneralTT/Syntax/All.vio GeneralTT/Typing/Context.vio GeneralTT/Typing/Judgement.vio GeneralTT/Typing/RawRule.vio GeneralTT/Typing/StructuralRule.vio GeneralTT/Typing/RawTypeTheory.vio GeneralTT/Auxiliary/WellFounded.vio GeneralTT/Presented/AlgebraicExtension.vio GeneralTT/Presented/PresentedRawRule.vio GeneralTT/Presented/PresentedRawTypeTheory.vio GeneralTT/Presented/TypedRule.vio GeneralTT/Presented/TypeTheory.vio GeneralTT/Metatheorem/UniqueTyping.vio GeneralTT/Metatheorem/Elimination.vio GeneralTT/Metatheorem/Presuppositions.vio GeneralTT/Metatheorem/Acceptability.vio GeneralTT/Example/ScopeSystemExamples.vio RegularCategories/DependentTypeTheory.vio
RegularCategories/Computability.vos RegularCategories/Computability.vok RegularCategories/Computability.required_vos: RegularCategories/Computability.v GeneralTT/Auxiliary/Family.vos GeneralTT/Auxiliary/Coproduct.vos GeneralTT/Syntax/ScopeSystem.vos GeneralTT/Syntax/All.vos GeneralTT/Typing/Context.vos GeneralTT/Typing/Judgement.vos GeneralTT/Typing/RawRule.vos GeneralTT/Typing/StructuralRule.vos GeneralTT/Typing/RawTypeTheory.vos GeneralTT/Auxiliary/WellFounded.vos GeneralTT/Presented/AlgebraicExtension.vos GeneralTT/Presented/PresentedRawRule.vos GeneralTT/Presented/PresentedRawTypeTheory.vos GeneralTT/Presented/TypedRule.vos GeneralTT/Presented/TypeTheory.vos GeneralTT/Metatheorem/UniqueTyping.vos GeneralTT/Metatheorem/Elimination.vos GeneralTT/Metatheorem/Presuppositions.vos GeneralTT/Metatheorem/Acceptability.vos GeneralTT/Example/ScopeSystemExamples.vos RegularCategories/DependentTypeTheory.vos