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
57184
log
plain
-rw-r--r--
cases.mli
1586
log
plain
-rw-r--r--
cbv.ml
14667
log
plain
-rw-r--r--
cbv.mli
2268
log
plain
-rwxr-xr-x
classops.ml
9458
log
plain
-rw-r--r--
classops.mli
3824
log
plain
-rw-r--r--
coercion.ml
7116
log
plain
-rw-r--r--
coercion.mli
1885
log
plain
-rw-r--r--
detyping.ml
11505
log
plain
-rw-r--r--
detyping.mli
1188
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
12597
log
plain
-rw-r--r--
evarconv.mli
965
log
plain
-rw-r--r--
evarutil.ml
18320
log
plain
-rw-r--r--
evarutil.mli
3059
log
plain
-rw-r--r--
evd.ml
2064
log
plain
-rw-r--r--
evd.mli
1802
log
plain
-rw-r--r--
indrec.ml
20253
log
plain
-rw-r--r--
indrec.mli
1861
log
plain
-rw-r--r--
inductiveops.ml
13082
log
plain
-rw-r--r--
inductiveops.mli
3262
log
plain
-rw-r--r--
instantiate.ml
1857
log
plain
-rw-r--r--
instantiate.mli
955
log
plain
-rw-r--r--
multcase.mli
901
log
plain
-rw-r--r--
pattern.ml
11818
log
plain
-rw-r--r--
pattern.mli
3302
log
plain
-rw-r--r--
pretype_errors.ml
5375
log
plain
-rw-r--r--
pretype_errors.mli
3091
log
plain
-rw-r--r--
pretyping.ml
20062
log
plain
-rw-r--r--
pretyping.mli
2721
log
plain
-rw-r--r--
rawterm.ml
3756
log
plain
-rw-r--r--
rawterm.mli
2608
log
plain
-rwxr-xr-x
recordops.ml
3631
log
plain
-rwxr-xr-x
recordops.mli
1699
log
plain
-rw-r--r--
reductionops.ml
29344
log
plain
-rw-r--r--
reductionops.mli
7895
log
plain
-rw-r--r--
retyping.ml
4932
log
plain
-rw-r--r--
retyping.mli
1429
log
plain
-rw-r--r--
syntax_def.ml
2242
log
plain
-rw-r--r--
syntax_def.mli
796
log
plain
-rw-r--r--
tacred.ml
27352
log
plain
-rw-r--r--
tacred.mli
2383
log
plain
-rw-r--r--
termops.ml
23699
log
plain
-rw-r--r--
termops.mli
5993
log
plain
-rw-r--r--
typing.ml
5110
log
plain
-rw-r--r--
typing.mli
924
log
plain