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
526
log
plain
-rw-r--r--
cClosure.ml
47381
log
plain
-rw-r--r--
cClosure.mli
7993
log
plain
-rw-r--r--
cPrimitives.ml
3858
log
plain
-rw-r--r--
cPrimitives.mli
1679
log
plain
-rw-r--r--
cbytecodes.ml
5200
log
plain
-rw-r--r--
cbytecodes.mli
3059
log
plain
-rw-r--r--
cbytegen.ml
32847
log
plain
-rw-r--r--
cbytegen.mli
1299
log
plain
-rw-r--r--
cemitcodes.ml
16485
log
plain
-rw-r--r--
cemitcodes.mli
1383
log
plain
-rw-r--r--
clambda.ml
25979
log
plain
-rw-r--r--
clambda.mli
1512
log
plain
-rw-r--r--
constr.ml
55371
log
plain
-rw-r--r--
constr.mli
25562
log
plain
-rw-r--r--
context.ml
18458
log
plain
-rw-r--r--
context.mli
13498
log
plain
-rw-r--r--
conv_oracle.ml
3773
log
plain
-rw-r--r--
conv_oracle.mli
1856
log
plain
-rw-r--r--
cooking.ml
8787
log
plain
-rw-r--r--
cooking.mli
1355
log
plain
-rw-r--r--
csymtable.ml
6136
log
plain
-rw-r--r--
csymtable.mli
923
log
plain
-rw-r--r--
declarations.ml
11831
log
plain
-rw-r--r--
declareops.ml
13739
log
plain
-rw-r--r--
declareops.mli
3250
log
plain
-rw-r--r--
doc.tex
277
log
plain
-rw-r--r--
dune
768
log
plain
-rw-r--r--
entries.ml
4562
log
plain
-rw-r--r--
environ.ml
24174
log
plain
-rw-r--r--
environ.mli
13421
log
plain
-rw-r--r--
esubst.ml
6859
log
plain
-rw-r--r--
esubst.mli
3437
log
plain
-rw-r--r--
evar.ml
877
log
plain
-rw-r--r--
evar.mli
1526
log
plain
-rw-r--r--
genOpcodeFiles.ml
4433
log
plain
-rw-r--r--
indTyping.ml
14579
log
plain
-rw-r--r--
indTyping.mli
1440
log
plain
-rw-r--r--
indtypes.ml
24524
log
plain
-rw-r--r--
indtypes.mli
1452
log
plain
-rw-r--r--
inductive.ml
49607
log
plain
-rw-r--r--
inductive.mli
5511
log
plain
-rw-r--r--
kernel.mllib
480
log
plain
-rw-r--r--
mod_subst.ml
18080
log
plain
-rw-r--r--
mod_subst.mli
5970
log
plain
-rw-r--r--
mod_typing.ml
14817
log
plain
-rw-r--r--
mod_typing.mli
2373
log
plain
-rw-r--r--
modops.ml
22162
log
plain
-rw-r--r--
modops.mli
5254
log
plain
-rw-r--r--
names.ml
30648
log
plain
-rw-r--r--
names.mli
19341
log
plain
-rw-r--r--
nativecode.ml
74350
log
plain
-rw-r--r--
nativecode.mli
2517
log
plain
-rw-r--r--
nativeconv.ml
7288
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
21097
log
plain
-rw-r--r--
nativelambda.mli
2943
log
plain
-rw-r--r--
nativelib.ml
5784
log
plain
-rw-r--r--
nativelib.mli
1381
log
plain
-rw-r--r--
nativelibrary.ml
2828
log
plain
-rw-r--r--
nativelibrary.mli
917
log
plain
-rw-r--r--
nativevalues.ml
13271
log
plain
-rw-r--r--
nativevalues.mli
5715
log
plain
-rw-r--r--
opaqueproof.ml
6061
log
plain
-rw-r--r--
opaqueproof.mli
3457
log
plain
-rw-r--r--
primred.ml
6542
log
plain
-rw-r--r--
primred.mli
1248
log
plain
-rw-r--r--
reduction.ml
38618
log
plain
-rw-r--r--
reduction.mli
5533
log
plain
-rw-r--r--
retroknowledge.ml
1576
log
plain
-rw-r--r--
retroknowledge.mli
1218
log
plain
-rw-r--r--
retypeops.ml
4767
log
plain
-rw-r--r--
retypeops.mli
1291
log
plain
-rw-r--r--
safe_typing.ml
45861
log
plain
-rw-r--r--
safe_typing.mli
7824
log
plain
-rw-r--r--
sorts.ml
3891
log
plain
-rw-r--r--
sorts.mli
1760
log
plain
-rw-r--r--
subtyping.ml
14518
log
plain
-rw-r--r--
subtyping.mli
799
log
plain
-rw-r--r--
term.ml
13811
log
plain
-rw-r--r--
term.mli
8461
log
plain
-rw-r--r--
term_typing.ml
15135
log
plain
-rw-r--r--
term_typing.mli
1855
log
plain
-rw-r--r--
transparentState.ml
1216
log
plain
-rw-r--r--
transparentState.mli
1078
log
plain
-rw-r--r--
type_errors.ml
8256
log
plain
-rw-r--r--
type_errors.mli
5594
log
plain
-rw-r--r--
typeops.ml
25343
log
plain
-rw-r--r--
typeops.mli
5248
log
plain
-rw-r--r--
uGraph.ml
7492
log
plain
-rw-r--r--
uGraph.mli
3542
log
plain
-rw-r--r--
uint63.mli
1095
log
plain
-rw-r--r--
uint63_amd64.ml
6255
log
plain
-rw-r--r--
uint63_x86.ml
7264
log
plain
-rw-r--r--
univ.ml
33694
log
plain
-rw-r--r--
univ.mli
14630
log
plain
-rw-r--r--
vars.ml
10243
log
plain
-rw-r--r--
vars.mli
6890
log
plain
-rw-r--r--
vconv.ml
7586
log
plain
-rw-r--r--
vconv.mli
1032
log
plain
-rw-r--r--
vm.ml
5971
log
plain
-rw-r--r--
vm.mli
1446
log
plain
-rw-r--r--
vmvalues.ml
23658
log
plain
-rw-r--r--
vmvalues.mli
4970
log
plain
-rw-r--r--
write_uint63.ml
1476
log
plain