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
13426
log
plain
-rw-r--r--
check.mllib
371
log
plain
-rw-r--r--
check_stat.ml
1889
log
plain
-rw-r--r--
check_stat.mli
609
log
plain
-rw-r--r--
checker.ml
11880
log
plain
-rw-r--r--
closure.ml
27921
log
plain
-rw-r--r--
closure.mli
5567
log
plain
-rw-r--r--
declarations.ml
26948
log
plain
-rw-r--r--
declarations.mli
6927
log
plain
-rw-r--r--
environ.ml
6295
log
plain
-rw-r--r--
environ.mli
2447
log
plain
-rw-r--r--
include
4778
log
plain
-rw-r--r--
indtypes.ml
20809
log
plain
-rw-r--r--
indtypes.mli
1356
log
plain
-rw-r--r--
inductive.ml
34120
log
plain
-rw-r--r--
inductive.mli
2995
log
plain
-rw-r--r--
main.ml
26
log
plain
-rw-r--r--
mod_checking.ml
12830
log
plain
-rw-r--r--
mod_checking.mli
614
log
plain
-rw-r--r--
modops.ml
5983
log
plain
-rw-r--r--
modops.mli
1811
log
plain
-rw-r--r--
reduction.ml
15773
log
plain
-rw-r--r--
reduction.mli
1833
log
plain
-rw-r--r--
safe_typing.ml
7061
log
plain
-rw-r--r--
safe_typing.mli
1353
log
plain
-rw-r--r--
subtyping.ml
14293
log
plain
-rw-r--r--
subtyping.mli
754
log
plain
-rw-r--r--
term.ml
16719
log
plain
-rw-r--r--
term.mli
4171
log
plain
-rw-r--r--
type_errors.ml
3657
log
plain
-rw-r--r--
type_errors.mli
3446
log
plain
-rw-r--r--
typeops.ml
13004
log
plain
-rw-r--r--
typeops.mli
967
log
plain
-rw-r--r--
validate.ml
6541
log
plain