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
55731
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
59922
log
plain
-rw-r--r--
constr.mli
25529
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
14767
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
4452
log
plain
-rw-r--r--
environ.ml
28733
log
plain
-rw-r--r--
environ.mli
15537
log
plain
-rw-r--r--
esubst.ml
7575
log
plain
-rw-r--r--
esubst.mli
4044
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
4864
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
54731
log
plain
-rw-r--r--
inductive.mli
5947
log
plain
-rw-r--r--
inferCumulativity.ml
10601
log
plain
-rw-r--r--
inferCumulativity.mli
1140
log
plain
-rw-r--r--
kernel.mllib
545
log
plain
-rw-r--r--
mod_subst.ml
18215
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
78786
log
plain
-rw-r--r--
nativecode.mli
2468
log
plain
-rw-r--r--
nativeconv.ml
7878
log
plain
-rw-r--r--
nativeconv.mli
1053
log
plain
-rw-r--r--
nativelambda.ml
23248
log
plain
-rw-r--r--
nativelambda.mli
3011
log
plain
-rw-r--r--
nativelib.ml
7512
log
plain
-rw-r--r--
nativelib.mli
1864
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
42925
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
54619
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
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
8626
log
plain
-rw-r--r--
type_errors.mli
5913
log
plain
-rw-r--r--
typeops.ml
28650
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
7581
log
plain
-rw-r--r--
uint63_63.ml
6523
log
plain
-rw-r--r--
univ.ml
34136
log
plain
-rw-r--r--
univ.mli
14939
log
plain
-rw-r--r--
vars.ml
11602
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
5319
log
plain
-rw-r--r--
vmbytecodes.mli
3096
log
plain
-rw-r--r--
vmbytegen.ml
33772
log
plain
-rw-r--r--
vmbytegen.mli
1319
log
plain
-rw-r--r--
vmemitcodes.ml
17932
log
plain
-rw-r--r--
vmemitcodes.mli
1571
log
plain
-rw-r--r--
vmlambda.ml
25199
log
plain
-rw-r--r--
vmlambda.mli
1459
log
plain
-rw-r--r--
vmsymtable.ml
7056
log
plain
-rw-r--r--
vmsymtable.mli
923
log
plain
-rw-r--r--
vmvalues.ml
24698
log
plain
-rw-r--r--
vmvalues.mli
5235
log
plain