-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy path_CoqProject
executable file
·105 lines (94 loc) · 2.86 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
93
94
95
96
97
98
99
100
101
102
103
104
105
# ===================================================================
# Copyright 2022 ZhengPu Shi
# This file is part of CoqMatrix. It is distributed under the MIT
# "expat license". You should have recieved a LICENSE file with it.
# ===================================================================
-I .
-R CoqMatrix CoqMatrix
-arg -w -arg -notation-overridden
-arg -w -arg -notation-incompatible-format
-arg -w -arg -deprecated-hint-without-locality
-arg -w -arg -redundant-canonical-projection
-arg -w -arg -ambiguous-paths
-arg -w -arg -local-declaration
-arg -w -arg -hiding-delimiting-key
# ===== CoqExt =====
CoqMatrix/CoqExt/CoqSetting.v
CoqMatrix/CoqExt/BasicConfig.v
CoqMatrix/CoqExt/FuncExt.v
CoqMatrix/CoqExt/TupleExt.v
CoqMatrix/CoqExt/BoolExt.v
CoqMatrix/CoqExt/QExt.v
CoqMatrix/CoqExt/QcExt.v
CoqMatrix/CoqExt/NatExt.v
CoqMatrix/CoqExt/ZExt.v
CoqMatrix/CoqExt/RExt.v
CoqMatrix/CoqExt/RAST.v
CoqMatrix/CoqExt/StrExt.v
CoqMatrix/CoqExt/ExtrOcamlR.v
CoqMatrix/CoqExt/SetoidListExt.v
CoqMatrix/CoqExt/SetoidListListExt.v
CoqMatrix/CoqExt/HierarchySetoid.v
CoqMatrix/CoqExt/Sequence.v
#CoqMatrix/CoqExt/MyExtrOCamlInt63.v
CoqMatrix/CoqExt/MyExtrOCamlPArray.v
CoqMatrix/CoqExt/Hierarchy.v
CoqMatrix/CoqExt/ListExt.v
# ===== Complex =====
CoqMatrix/Complex/Complex.v
# ===== Calculus =====
CoqMatrix/Calculus/RealFunction.v
CoqMatrix/Calculus/Derivative.v
CoqMatrix/Calculus/Integration.v
CoqMatrix/Calculus/Calculus.v
# ===== CoqMatrix =====
CoqMatrix/ElementType.v
CoqMatrix/MatrixTheory.v
CoqMatrix/VectorTheory.v
CoqMatrix/DepRec/Matrix.v
CoqMatrix/DepRec/MatrixTheoryDR.v
CoqMatrix/DepRec/VectorTheoryDR.v
CoqMatrix/DepList/Matrix.v
CoqMatrix/DepList/MatrixTheoryDL.v
CoqMatrix/DepList/VectorTheoryDL.v
CoqMatrix/DepPair/Vector.v
CoqMatrix/DepPair/Matrix.v
CoqMatrix/DepPair/MatrixTheoryDP.v
CoqMatrix/DepPair/VectorTheoryDP.v
CoqMatrix/NatFun/Matrix.v
CoqMatrix/NatFun/MatrixTheoryNF.v
CoqMatrix/NatFun/VectorTheoryNF.v
CoqMatrix/SafeNatFun/Matrix.v
CoqMatrix/SafeNatFun/MatrixTheorySF.v
CoqMatrix/SafeNatFun/Vector.v
CoqMatrix/SafeNatFun/VectorTheorySF.v
CoqMatrix/SafeNatFun2/vec.v
CoqMatrix/SafeNatFun2/MatrixTheorySF2.v
CoqMatrix/SafeNatFun2/VectorTheorySF2.v
# CoqMatrix/FinFun/Matrix.v
# CoqMatrix/FinFun/MatrixTheoryFF.v
CoqMatrix/MatrixAll.v
CoqMatrix/MatrixHomo/HomomorphismThy.v
CoqMatrix/MatrixHomo/IsomorphismThy.v
CoqMatrix/MatrixHomo/MatrixHomomorphism.v
CoqMatrix/MatrixHomo/MatrixIsomorphism.v
CoqMatrix/VectorAll.v
CoqMatrix/MatrixNat.v
CoqMatrix/MatrixZ.v
CoqMatrix/MatrixQ.v
CoqMatrix/MatrixQc.v
CoqMatrix/MatrixR.v
CoqMatrix/MatrixC.v
CoqMatrix/VectorNat.v
CoqMatrix/VectorZ.v
CoqMatrix/VectorQ.v
CoqMatrix/VectorQc.v
CoqMatrix/VectorR.v
CoqMatrix/VectorC.v
#CoqMatrix/NatFun/Inversion.v
#CoqMatrix/DepRec/VectorR.v
#CoqMatrix/NatFun/VectorR.v
#CoqMatrix/OCamlExtractionComparison/matrix.v
CoqMatrix/examples.v
# ===== LinearAlgebra =====
CoqMatrix/LinearAlgebra/PermutationExt.v