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
55538
log
plain
-rw-r--r--
cClosure.mli
8659
log
plain
-rw-r--r--
cPrimitives.ml
12739
log
plain
-rw-r--r--
cPrimitives.mli
3654
log
plain
-rw-r--r--
cbytecodes.ml
5463
log
plain
-rw-r--r--
cbytecodes.mli
3134
log
plain
-rw-r--r--
cbytegen.ml
34490
log
plain
-rw-r--r--
cbytegen.mli
1317
log
plain
-rw-r--r--
cemitcodes.ml
17813
log
plain
-rw-r--r--
cemitcodes.mli
1570
log
plain
-rw-r--r--
clambda.ml
26810
log
plain
-rw-r--r--
clambda.mli
1543
log
plain
-rw-r--r--
constr.ml
62069
log
plain
-rw-r--r--
constr.mli
26716
log
plain
-rw-r--r--
context.ml
18323
log
plain
-rw-r--r--
context.mli
13502
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
14753
log
plain
-rw-r--r--
cooking.mli
1527
log
plain
-rw-r--r--
csymtable.ml
7416
log
plain
-rw-r--r--
csymtable.mli
923
log
plain
-rw-r--r--
declarations.ml
12403
log
plain
-rw-r--r--
declareops.ml
14581
log
plain
-rw-r--r--
declareops.mli
3373
log
plain
-rw-r--r--
doc.tex
277
log
plain
-rw-r--r--
dune
688
log
plain
-rw-r--r--
entries.ml
4336
log
plain
-rw-r--r--
environ.ml
26102
log
plain
-rw-r--r--
environ.mli
14772
log
plain
-rw-r--r--
esubst.ml
6859
log
plain
-rw-r--r--
esubst.mli
3436
log
plain
-rw-r--r--
evar.ml
877
log
plain
-rw-r--r--
evar.mli
1526
log
plain
-rw-r--r--
float64.ml
5484
log
plain
-rw-r--r--
float64.mli
2935
log
plain
-rw-r--r--
genOpcodeFiles.ml
4985
log
plain
-rw-r--r--
indTyping.ml
16716
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
54109
log
plain
-rw-r--r--
inductive.mli
5947
log
plain
-rw-r--r--
inferCumulativity.ml
8924
log
plain
-rw-r--r--
inferCumulativity.mli
1104
log
plain
-rw-r--r--
kernel.mllib
524
log
plain
-rw-r--r--
mod_subst.ml
18663
log
plain
-rw-r--r--
mod_subst.mli
5970
log
plain
-rw-r--r--
mod_typing.ml
14776
log
plain
-rw-r--r--
mod_typing.mli
2433
log
plain
-rw-r--r--
modops.ml
22372
log
plain
-rw-r--r--
modops.mli
5254
log
plain
-rw-r--r--
names.ml
30898
log
plain
-rw-r--r--
names.mli
19748
log
plain
-rw-r--r--
nativecode.ml
79206
log
plain
-rw-r--r--
nativecode.mli
2483
log
plain
-rw-r--r--
nativeconv.ml
7845
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
23299
log
plain
-rw-r--r--
nativelambda.mli
3011
log
plain
-rw-r--r--
nativelib.ml
7203
log
plain
-rw-r--r--
nativelib.mli
1980
log
plain
-rw-r--r--
nativelibrary.ml
2912
log
plain
-rw-r--r--
nativelibrary.mli
930
log
plain
-rw-r--r--
nativevalues.ml
19439
log
plain
-rw-r--r--
nativevalues.mli
8808
log
plain
-rw-r--r--
opaqueproof.ml
5013
log
plain
-rw-r--r--
opaqueproof.mli
2692
log
plain
-rw-r--r--
parray.ml
3508
log
plain
-rw-r--r--
parray.mli
1522
log
plain
-rw-r--r--
primred.ml
13088
log
plain
-rw-r--r--
primred.mli
2608
log
plain
-rw-r--r--
reduction.ml
41146
log
plain
-rw-r--r--
reduction.mli
5601
log
plain
-rw-r--r--
relevanceops.ml
4901
log
plain
-rw-r--r--
relevanceops.mli
1414
log
plain
-rw-r--r--
retroknowledge.ml
2281
log
plain
-rw-r--r--
retroknowledge.mli
1825
log
plain
-rw-r--r--
safe_typing.ml
54048
log
plain
-rw-r--r--
safe_typing.mli
8023
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
14838
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
15442
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
8398
log
plain
-rw-r--r--
type_errors.mli
5737
log
plain
-rw-r--r--
typeops.ml
28647
log
plain
-rw-r--r--
typeops.mli
5379
log
plain
-rw-r--r--
uGraph.ml
7679
log
plain
-rw-r--r--
uGraph.mli
3686
log
plain
-rw-r--r--
uint63.mli
2394
log
plain
-rw-r--r--
uint63_31.ml
7717
log
plain
-rw-r--r--
uint63_63.ml
6699
log
plain
-rw-r--r--
univ.ml
34396
log
plain
-rw-r--r--
univ.mli
14939
log
plain
-rw-r--r--
vars.ml
11464
log
plain
-rw-r--r--
vars.mli
6746
log
plain
-rw-r--r--
vconv.ml
8102
log
plain
-rw-r--r--
vconv.mli
1032
log
plain
-rw-r--r--
vm.ml
6137
log
plain
-rw-r--r--
vm.mli
1446
log
plain
-rw-r--r--
vmvalues.ml
24774
log
plain
-rw-r--r--
vmvalues.mli
5357
log
plain