index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
Mode
Name
Size
-rw-r--r--
cases.ml
66960
log
plain
-rw-r--r--
cases.mli
2436
log
plain
-rw-r--r--
cbv.ml
14344
log
plain
-rw-r--r--
cbv.mli
2059
log
plain
-rw-r--r--
classops.ml
12580
log
plain
-rw-r--r--
classops.mli
3414
log
plain
-rw-r--r--
coercion.ml
10337
log
plain
-rw-r--r--
coercion.mli
2883
log
plain
-rw-r--r--
detyping.ml
24919
log
plain
-rw-r--r--
detyping.mli
2260
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
20880
log
plain
-rw-r--r--
evarconv.mli
1528
log
plain
-rw-r--r--
evarutil.ml
56914
log
plain
-rw-r--r--
evarutil.mli
7985
log
plain
-rw-r--r--
evd.ml
28354
log
plain
-rw-r--r--
evd.mli
10737
log
plain
-rw-r--r--
indrec.ml
19570
log
plain
-rw-r--r--
indrec.mli
2367
log
plain
-rw-r--r--
inductiveops.ml
16699
log
plain
-rw-r--r--
inductiveops.mli
5132
log
plain
-rw-r--r--
matching.ml
11301
log
plain
-rw-r--r--
matching.mli
3588
log
plain
-rw-r--r--
namegen.ml
10961
log
plain
-rw-r--r--
namegen.mli
3319
log
plain
-rw-r--r--
pattern.ml
12262
log
plain
-rw-r--r--
pattern.mli
2686
log
plain
-rw-r--r--
pretype_errors.ml
6740
log
plain
-rw-r--r--
pretype_errors.mli
3883
log
plain
-rw-r--r--
pretyping.ml
27046
log
plain
-rw-r--r--
pretyping.mli
3811
log
plain
-rw-r--r--
pretyping.mllib
251
log
plain
-rw-r--r--
rawterm.ml
12774
log
plain
-rw-r--r--
rawterm.mli
5548
log
plain
-rw-r--r--
recordops.ml
11281
log
plain
-rwxr-xr-x
recordops.mli
2985
log
plain
-rw-r--r--
reductionops.ml
32453
log
plain
-rw-r--r--
reductionops.mli
8953
log
plain
-rw-r--r--
retyping.ml
7034
log
plain
-rw-r--r--
retyping.mli
1488
log
plain
-rw-r--r--
tacred.ml
33945
log
plain
-rw-r--r--
tacred.mli
3317
log
plain
-rw-r--r--
term_dnet.ml
13141
log
plain
-rw-r--r--
term_dnet.mli
3436
log
plain
-rw-r--r--
termops.ml
33484
log
plain
-rw-r--r--
termops.mli
9881
log
plain
-rw-r--r--
typeclasses.ml
11757
log
plain
-rw-r--r--
typeclasses.mli
3410
log
plain
-rw-r--r--
typeclasses_errors.ml
2019
log
plain
-rw-r--r--
typeclasses_errors.mli
1480
log
plain
-rw-r--r--
typing.ml
7261
log
plain
-rw-r--r--
typing.mli
1170
log
plain
-rw-r--r--
unification.ml
36213
log
plain
-rw-r--r--
unification.mli
1988
log
plain
-rw-r--r--
vnorm.ml
10414
log
plain
-rw-r--r--
vnorm.mli
643
log
plain