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
8656
log
plain
-rw-r--r--
cPrimitives.ml
12562
log
plain
-rw-r--r--
cPrimitives.mli
3638
log
plain
-rw-r--r--
constr.ml
62138
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
14762
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
838
log
plain
-rw-r--r--
entries.ml
4336
log
plain
-rw-r--r--
environ.ml
27489
log
plain
-rw-r--r--
environ.mli
15602
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.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
4938
log
plain
-rw-r--r--
indTyping.ml
16696
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
54176
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
545
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
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
31510
log
plain
-rw-r--r--
names.mli
21205
log
plain
-rw-r--r--
nativecode.ml
79353
log
plain
-rw-r--r--
nativecode.mli
2483
log
plain
-rw-r--r--
nativeconv.ml
7882
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
23301
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
19265
log
plain
-rw-r--r--
nativevalues.mli
8699
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
12974
log
plain
-rw-r--r--
primred.mli
2608
log
plain
-rw-r--r--
reduction.ml
42641
log
plain
-rw-r--r--
reduction.mli
5498
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
54423
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
14821
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
15446
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
28657
log
plain
-rw-r--r--
typeops.mli
5366
log
plain
-rw-r--r--
uGraph.ml
8423
log
plain
-rw-r--r--
uGraph.mli
4065
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
34136
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
8120
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
5466
log
plain
-rw-r--r--
vmbytecodes.mli
3134
log
plain
-rw-r--r--
vmbytegen.ml
34133
log
plain
-rw-r--r--
vmbytegen.mli
1319
log
plain
-rw-r--r--
vmemitcodes.ml
17770
log
plain
-rw-r--r--
vmemitcodes.mli
1571
log
plain
-rw-r--r--
vmlambda.ml
26813
log
plain
-rw-r--r--
vmlambda.mli
1543
log
plain
-rw-r--r--
vmsymtable.ml
7056
log
plain
-rw-r--r--
vmsymtable.mli
923
log
plain
-rw-r--r--
vmvalues.ml
24460
log
plain
-rw-r--r--
vmvalues.mli
5235
log
plain