index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
Mode
Name
Size
-rw-r--r--
.merlin.in
109
log
plain
d---------
byterun
531
log
plain
-rw-r--r--
cClosure.ml
58548
log
plain
-rw-r--r--
cClosure.mli
8785
log
plain
-rw-r--r--
cPrimitives.ml
13598
log
plain
-rw-r--r--
cPrimitives.mli
3735
log
plain
-rw-r--r--
constr.ml
61857
log
plain
-rw-r--r--
constr.mli
24854
log
plain
-rw-r--r--
context.ml
18569
log
plain
-rw-r--r--
context.mli
13627
log
plain
-rw-r--r--
conv_oracle.ml
3918
log
plain
-rw-r--r--
conv_oracle.mli
1883
log
plain
-rw-r--r--
cooking.ml
14612
log
plain
-rw-r--r--
cooking.mli
1527
log
plain
-rw-r--r--
declarations.ml
12404
log
plain
-rw-r--r--
declareops.ml
14609
log
plain
-rw-r--r--
declareops.mli
3373
log
plain
-rw-r--r--
doc.tex
277
log
plain
-rw-r--r--
dune
848
log
plain
-rw-r--r--
entries.ml
4452
log
plain
-rw-r--r--
environ.ml
28889
log
plain
-rw-r--r--
environ.mli
15599
log
plain
-rw-r--r--
esubst.ml
8417
log
plain
-rw-r--r--
esubst.mli
4443
log
plain
-rw-r--r--
evar.ml
877
log
plain
-rw-r--r--
evar.mli
1526
log
plain
-rw-r--r--
float64.mli
2935
log
plain
-rw-r--r--
float64_31.ml
1559
log
plain
-rw-r--r--
float64_63.ml
1459
log
plain
-rw-r--r--
float64_common.ml
4624
log
plain
-rw-r--r--
float64_common.mli
2832
log
plain
-rw-r--r--
genOpcodeFiles.ml
5417
log
plain
-rw-r--r--
indTyping.ml
16877
log
plain
-rw-r--r--
indTyping.mli
1868
log
plain
-rw-r--r--
indtypes.ml
26147
log
plain
-rw-r--r--
indtypes.mli
889
log
plain
-rw-r--r--
inductive.ml
58324
log
plain
-rw-r--r--
inductive.mli
6863
log
plain
-rw-r--r--
inferCumulativity.ml
10969
log
plain
-rw-r--r--
inferCumulativity.mli
1140
log
plain
-rw-r--r--
kernel.mllib
545
log
plain
-rw-r--r--
mod_subst.ml
18418
log
plain
-rw-r--r--
mod_subst.mli
5558
log
plain
-rw-r--r--
mod_typing.ml
14642
log
plain
-rw-r--r--
mod_typing.mli
2433
log
plain
-rw-r--r--
modops.ml
22374
log
plain
-rw-r--r--
modops.mli
5254
log
plain
-rw-r--r--
names.ml
33124
log
plain
-rw-r--r--
names.mli
22145
log
plain
-rw-r--r--
nativecode.ml
78856
log
plain
-rw-r--r--
nativecode.mli
2577
log
plain
-rw-r--r--
nativeconv.ml
7999
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
23224
log
plain
-rw-r--r--
nativelambda.mli
3011
log
plain
-rw-r--r--
nativelib.ml
7717
log
plain
-rw-r--r--
nativelib.mli
2210
log
plain
-rw-r--r--
nativelibrary.ml
2770
log
plain
-rw-r--r--
nativelibrary.mli
917
log
plain
-rw-r--r--
nativevalues.ml
20446
log
plain
-rw-r--r--
nativevalues.mli
9207
log
plain
-rw-r--r--
opaqueproof.ml
5013
log
plain
-rw-r--r--
opaqueproof.mli
2692
log
plain
-rw-r--r--
parray.ml
3159
log
plain
-rw-r--r--
parray.mli
1495
log
plain
-rw-r--r--
primred.ml
13646
log
plain
-rw-r--r--
primred.mli
2608
log
plain
-rw-r--r--
reduction.ml
46675
log
plain
-rw-r--r--
reduction.mli
5498
log
plain
-rw-r--r--
relevanceops.ml
4919
log
plain
-rw-r--r--
relevanceops.mli
1414
log
plain
-rw-r--r--
retroknowledge.ml
2222
log
plain
-rw-r--r--
retroknowledge.mli
1789
log
plain
-rw-r--r--
safe_typing.ml
54615
log
plain
-rw-r--r--
safe_typing.mli
8077
log
plain
-rw-r--r--
section.ml
6416
log
plain
-rw-r--r--
section.mli
3698
log
plain
-rw-r--r--
sorts.ml
3897
log
plain
-rw-r--r--
sorts.mli
1709
log
plain
-rw-r--r--
subtyping.ml
14272
log
plain
-rw-r--r--
subtyping.mli
799
log
plain
-rw-r--r--
term.ml
13055
log
plain
-rw-r--r--
term.mli
8099
log
plain
-rw-r--r--
term_typing.ml
15319
log
plain
-rw-r--r--
term_typing.mli
2057
log
plain
-rw-r--r--
transparentState.ml
1216
log
plain
-rw-r--r--
transparentState.mli
1078
log
plain
-rw-r--r--
type_errors.ml
8626
log
plain
-rw-r--r--
type_errors.mli
5913
log
plain
-rw-r--r--
typeops.ml
28741
log
plain
-rw-r--r--
typeops.mli
5178
log
plain
-rw-r--r--
uGraph.ml
8799
log
plain
-rw-r--r--
uGraph.mli
4084
log
plain
-rw-r--r--
uint63.mli
2637
log
plain
-rw-r--r--
uint63_31.ml
8659
log
plain
-rw-r--r--
uint63_63.ml
6964
log
plain
-rw-r--r--
univ.ml
34136
log
plain
-rw-r--r--
univ.mli
14939
log
plain
-rw-r--r--
vars.ml
12128
log
plain
-rw-r--r--
vars.mli
6746
log
plain
-rw-r--r--
vconv.ml
8166
log
plain
-rw-r--r--
vconv.mli
1032
log
plain
-rw-r--r--
vm.ml
6112
log
plain
-rw-r--r--
vm.mli
1446
log
plain
-rw-r--r--
vmbytecodes.ml
5347
log
plain
-rw-r--r--
vmbytecodes.mli
3177
log
plain
-rw-r--r--
vmbytegen.ml
33882
log
plain
-rw-r--r--
vmbytegen.mli
1345
log
plain
-rw-r--r--
vmemitcodes.ml
18661
log
plain
-rw-r--r--
vmemitcodes.mli
1571
log
plain
-rw-r--r--
vmlambda.ml
25385
log
plain
-rw-r--r--
vmlambda.mli
1493
log
plain
-rw-r--r--
vmsymtable.ml
7122
log
plain
-rw-r--r--
vmsymtable.mli
957
log
plain
-rw-r--r--
vmvalues.ml
24641
log
plain
-rw-r--r--
vmvalues.mli
5167
log
plain