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
6982
log
plain
-rw-r--r--
Makefile
2022
log
plain
-rw-r--r--
check.ml
12049
log
plain
-rw-r--r--
check_stat.ml
1922
log
plain
-rw-r--r--
check_stat.mli
609
log
plain
-rw-r--r--
checker.ml
11564
log
plain
-rw-r--r--
closure.ml
34719
log
plain
-rw-r--r--
closure.mli
6224
log
plain
-rw-r--r--
declarations.ml
16774
log
plain
-rw-r--r--
declarations.mli
5875
log
plain
-rw-r--r--
environ.ml
5801
log
plain
-rw-r--r--
indtypes.ml
21371
log
plain
-rw-r--r--
indtypes.mli
1444
log
plain
-rw-r--r--
inductive.ml
33225
log
plain
-rw-r--r--
inductive.mli
2959
log
plain
-rw-r--r--
main.ml
26
log
plain
-rw-r--r--
mod_checking.ml
13275
log
plain
-rw-r--r--
modops.ml
16258
log
plain
-rw-r--r--
modops.mli
2214
log
plain
-rw-r--r--
reduction.ml
13465
log
plain
-rw-r--r--
reduction.mli
1999
log
plain
-rw-r--r--
safe_typing.ml
8056
log
plain
-rw-r--r--
safe_typing.mli
922
log
plain
-rw-r--r--
subtyping.ml
14420
log
plain
-rw-r--r--
subtyping.mli
800
log
plain
-rw-r--r--
term.ml
14847
log
plain
-rw-r--r--
type_errors.ml
3805
log
plain
-rw-r--r--
type_errors.mli
3585
log
plain
-rw-r--r--
typeops.ml
13234
log
plain
-rw-r--r--
typeops.mli
950
log
plain
-rw-r--r--
validate.ml
6746
log
plain