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
13386
log
plain
-rw-r--r--
check.mllib
265
log
plain
-rw-r--r--
check_stat.ml
1906
log
plain
-rw-r--r--
check_stat.mli
609
log
plain
-rw-r--r--
checker.ml
11993
log
plain
-rw-r--r--
closure.ml
34293
log
plain
-rw-r--r--
closure.mli
6222
log
plain
-rw-r--r--
declarations.ml
21004
log
plain
-rw-r--r--
declarations.mli
6359
log
plain
-rw-r--r--
environ.ml
5702
log
plain
-rw-r--r--
environ.mli
2686
log
plain
-rw-r--r--
include
4628
log
plain
-rw-r--r--
indtypes.ml
20448
log
plain
-rw-r--r--
indtypes.mli
1444
log
plain
-rw-r--r--
inductive.ml
33278
log
plain
-rw-r--r--
inductive.mli
2959
log
plain
-rw-r--r--
main.ml
26
log
plain
-rw-r--r--
mod_checking.ml
13954
log
plain
-rw-r--r--
modops.ml
11302
log
plain
-rw-r--r--
modops.mli
2286
log
plain
-rw-r--r--
reduction.ml
15918
log
plain
-rw-r--r--
reduction.mli
2138
log
plain
-rw-r--r--
safe_typing.ml
4658
log
plain
-rw-r--r--
safe_typing.mli
974
log
plain
-rw-r--r--
subtyping.ml
14369
log
plain
-rw-r--r--
subtyping.mli
800
log
plain
-rw-r--r--
term.ml
16494
log
plain
-rw-r--r--
term.mli
4511
log
plain
-rw-r--r--
type_errors.ml
3803
log
plain
-rw-r--r--
type_errors.mli
3579
log
plain
-rw-r--r--
typeops.ml
14098
log
plain
-rw-r--r--
typeops.mli
1030
log
plain
-rw-r--r--
validate.ml
5606
log
plain