index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
Mode
Name
Size
-rw-r--r--
.depend
3051
log
plain
-rw-r--r--
Makefile
2059
log
plain
-rw-r--r--
check.ml
15443
log
plain
-rw-r--r--
check.mllib
493
log
plain
-rw-r--r--
check_stat.ml
1898
log
plain
-rw-r--r--
check_stat.mli
609
log
plain
-rw-r--r--
checker.ml
13776
log
plain
-rw-r--r--
cic.mli
15006
log
plain
-rw-r--r--
closure.ml
29076
log
plain
-rw-r--r--
closure.mli
5954
log
plain
-rw-r--r--
declarations.ml
19169
log
plain
-rw-r--r--
declarations.mli
1599
log
plain
-rw-r--r--
environ.ml
6789
log
plain
-rw-r--r--
environ.mli
2314
log
plain
-rw-r--r--
include
4965
log
plain
-rw-r--r--
indtypes.ml
20774
log
plain
-rw-r--r--
indtypes.mli
1314
log
plain
-rw-r--r--
inductive.ml
44800
log
plain
-rw-r--r--
inductive.mli
2913
log
plain
-rw-r--r--
main.ml
26
log
plain
-rw-r--r--
mod_checking.ml
4654
log
plain
-rw-r--r--
mod_checking.mli
605
log
plain
-rw-r--r--
modops.ml
4875
log
plain
-rw-r--r--
modops.mli
1505
log
plain
-rw-r--r--
print.ml
5065
log
plain
-rw-r--r--
reduction.ml
19236
log
plain
-rw-r--r--
reduction.mli
1903
log
plain
-rw-r--r--
safe_typing.ml
3165
log
plain
-rw-r--r--
safe_typing.mli
842
log
plain
-rw-r--r--
subtyping.ml
15368
log
plain
-rw-r--r--
subtyping.mli
725
log
plain
-rw-r--r--
term.ml
14158
log
plain
-rw-r--r--
term.mli
2461
log
plain
-rw-r--r--
type_errors.ml
3841
log
plain
-rw-r--r--
type_errors.mli
3604
log
plain
-rw-r--r--
typeops.ml
12656
log
plain
-rw-r--r--
typeops.mli
883
log
plain
-rw-r--r--
univ.ml
35098
log
plain
-rw-r--r--
univ.mli
7034
log
plain
-rw-r--r--
validate.ml
5126
log
plain
-rw-r--r--
values.ml
10531
log
plain
-rw-r--r--
votour.ml
7504
log
plain