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
13901
log
plain
-rw-r--r--
check.mllib
384
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
11792
log
plain
-rw-r--r--
cic.mli
11743
log
plain
-rw-r--r--
closure.ml
27561
log
plain
-rw-r--r--
closure.mli
5566
log
plain
-rw-r--r--
declarations.ml
18082
log
plain
-rw-r--r--
declarations.mli
1513
log
plain
-rw-r--r--
environ.ml
5617
log
plain
-rw-r--r--
environ.mli
2060
log
plain
-rw-r--r--
include
4778
log
plain
-rw-r--r--
indtypes.ml
20683
log
plain
-rw-r--r--
indtypes.mli
1337
log
plain
-rw-r--r--
inductive.ml
33822
log
plain
-rw-r--r--
inductive.mli
2976
log
plain
-rw-r--r--
main.ml
26
log
plain
-rw-r--r--
mod_checking.ml
12719
log
plain
-rw-r--r--
mod_checking.mli
605
log
plain
-rw-r--r--
modops.ml
5992
log
plain
-rw-r--r--
modops.mli
1792
log
plain
-rw-r--r--
reduction.ml
15782
log
plain
-rw-r--r--
reduction.mli
1842
log
plain
-rw-r--r--
safe_typing.ml
2994
log
plain
-rw-r--r--
safe_typing.mli
805
log
plain
-rw-r--r--
subtyping.ml
14086
log
plain
-rw-r--r--
subtyping.mli
725
log
plain
-rw-r--r--
term.ml
12555
log
plain
-rw-r--r--
term.mli
2204
log
plain
-rw-r--r--
type_errors.ml
3666
log
plain
-rw-r--r--
type_errors.mli
3445
log
plain
-rw-r--r--
typeops.ml
11621
log
plain
-rw-r--r--
typeops.mli
907
log
plain
-rw-r--r--
validate.ml
4582
log
plain
-rw-r--r--
values.ml
7780
log
plain
-rw-r--r--
votour.ml
5096
log
plain