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
567
log
plain
-rw-r--r--
cClosure.ml
51283
log
plain
-rw-r--r--
cClosure.mli
7953
log
plain
-rw-r--r--
cPrimitives.ml
6419
log
plain
-rw-r--r--
cPrimitives.mli
2363
log
plain
-rw-r--r--
cbytecodes.ml
5200
log
plain
-rw-r--r--
cbytecodes.mli
3059
log
plain
-rw-r--r--
cbytegen.ml
32921
log
plain
-rw-r--r--
cbytegen.mli
1310
log
plain
-rw-r--r--
cemitcodes.ml
17242
log
plain
-rw-r--r--
cemitcodes.mli
1533
log
plain
-rw-r--r--
clambda.ml
26102
log
plain
-rw-r--r--
clambda.mli
1543
log
plain
-rw-r--r--
constr.ml
55923
log
plain
-rw-r--r--
constr.mli
25666
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
13150
log
plain
-rw-r--r--
cooking.mli
1536
log
plain
-rw-r--r--
csymtable.ml
6628
log
plain
-rw-r--r--
csymtable.mli
923
log
plain
-rw-r--r--
declarations.ml
12190
log
plain
-rw-r--r--
declareops.ml
13517
log
plain
-rw-r--r--
declareops.mli
3306
log
plain
-rw-r--r--
doc.tex
277
log
plain
-rw-r--r--
dune
688
log
plain
-rw-r--r--
entries.ml
4405
log
plain
-rw-r--r--
environ.ml
26013
log
plain
-rw-r--r--
environ.mli
14150
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--
float64.ml
5045
log
plain
-rw-r--r--
float64.mli
2509
log
plain
-rw-r--r--
genOpcodeFiles.ml
4875
log
plain
-rw-r--r--
indTyping.ml
16300
log
plain
-rw-r--r--
indTyping.mli
1710
log
plain
-rw-r--r--
indtypes.ml
24088
log
plain
-rw-r--r--
indtypes.mli
848
log
plain
-rw-r--r--
inductive.ml
49961
log
plain
-rw-r--r--
inductive.mli
5505
log
plain
-rw-r--r--
inferCumulativity.ml
8983
log
plain
-rw-r--r--
inferCumulativity.mli
851
log
plain
-rw-r--r--
kernel.mllib
514
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
14885
log
plain
-rw-r--r--
mod_typing.mli
2373
log
plain
-rw-r--r--
modops.ml
21991
log
plain
-rw-r--r--
modops.mli
5254
log
plain
-rw-r--r--
names.ml
30842
log
plain
-rw-r--r--
names.mli
19699
log
plain
-rw-r--r--
nativecode.ml
76922
log
plain
-rw-r--r--
nativecode.mli
2483
log
plain
-rw-r--r--
nativeconv.ml
7280
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
22426
log
plain
-rw-r--r--
nativelambda.mli
2968
log
plain
-rw-r--r--
nativelib.ml
6240
log
plain
-rw-r--r--
nativelib.mli
1915
log
plain
-rw-r--r--
nativelibrary.ml
2828
log
plain
-rw-r--r--
nativelibrary.mli
930
log
plain
-rw-r--r--
nativevalues.ml
17685
log
plain
-rw-r--r--
nativevalues.mli
7813
log
plain
-rw-r--r--
opaqueproof.ml
5014
log
plain
-rw-r--r--
opaqueproof.mli
2692
log
plain
-rw-r--r--
primred.ml
11278
log
plain
-rw-r--r--
primred.mli
2130
log
plain
-rw-r--r--
reduction.ml
39138
log
plain
-rw-r--r--
reduction.mli
5533
log
plain
-rw-r--r--
retroknowledge.ml
2217
log
plain
-rw-r--r--
retroknowledge.mli
1785
log
plain
-rw-r--r--
retypeops.ml
4981
log
plain
-rw-r--r--
retypeops.mli
1441
log
plain
-rw-r--r--
safe_typing.ml
51839
log
plain
-rw-r--r--
safe_typing.mli
7920
log
plain
-rw-r--r--
section.ml
7284
log
plain
-rw-r--r--
section.mli
3402
log
plain
-rw-r--r--
sorts.ml
3832
log
plain
-rw-r--r--
sorts.mli
1677
log
plain
-rw-r--r--
subtyping.ml
14594
log
plain
-rw-r--r--
subtyping.mli
799
log
plain
-rw-r--r--
term.ml
13821
log
plain
-rw-r--r--
term.mli
8461
log
plain
-rw-r--r--
term_typing.ml
13985
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
8251
log
plain
-rw-r--r--
type_errors.mli
5584
log
plain
-rw-r--r--
typeops.ml
25412
log
plain
-rw-r--r--
typeops.mli
4969
log
plain
-rw-r--r--
uGraph.ml
7522
log
plain
-rw-r--r--
uGraph.mli
3585
log
plain
-rw-r--r--
uint63.mli
2394
log
plain
-rw-r--r--
uint63_31.ml
7607
log
plain
-rw-r--r--
uint63_63.ml
6699
log
plain
-rw-r--r--
univ.ml
33640
log
plain
-rw-r--r--
univ.mli
14631
log
plain
-rw-r--r--
vars.ml
10243
log
plain
-rw-r--r--
vars.mli
6890
log
plain
-rw-r--r--
vconv.ml
7723
log
plain
-rw-r--r--
vconv.mli
1032
log
plain
-rw-r--r--
vm.ml
5989
log
plain
-rw-r--r--
vm.mli
1446
log
plain
-rw-r--r--
vmvalues.ml
24318
log
plain
-rw-r--r--
vmvalues.mli
5021
log
plain