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
66707
log
plain
-rw-r--r--
cases.mli
1845
log
plain
-rw-r--r--
cbv.ml
13044
log
plain
-rw-r--r--
cbv.mli
1988
log
plain
-rwxr-xr-x
classops.ml
11698
log
plain
-rw-r--r--
classops.mli
3739
log
plain
-rw-r--r--
coercion.ml
7447
log
plain
-rw-r--r--
coercion.mli
1831
log
plain
-rw-r--r--
detyping.ml
18741
log
plain
-rw-r--r--
detyping.mli
1502
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
13975
log
plain
-rw-r--r--
evarconv.mli
960
log
plain
-rw-r--r--
evarutil.ml
20315
log
plain
-rw-r--r--
evarutil.mli
3376
log
plain
-rw-r--r--
evd.ml
1819
log
plain
-rw-r--r--
evd.mli
1701
log
plain
-rw-r--r--
indrec.ml
19872
log
plain
-rw-r--r--
indrec.mli
1947
log
plain
-rw-r--r--
inductiveops.ml
12216
log
plain
-rw-r--r--
inductiveops.mli
4094
log
plain
-rw-r--r--
instantiate.ml
1964
log
plain
-rw-r--r--
instantiate.mli
953
log
plain
-rw-r--r--
matching.ml
9096
log
plain
-rw-r--r--
matching.mli
1912
log
plain
-rw-r--r--
pattern.ml
10391
log
plain
-rw-r--r--
pattern.mli
2861
log
plain
-rw-r--r--
pretype_errors.ml
5371
log
plain
-rw-r--r--
pretype_errors.mli
3025
log
plain
-rw-r--r--
pretyping.ml
40947
log
plain
-rw-r--r--
pretyping.mli
2918
log
plain
-rw-r--r--
rawterm.ml
12861
log
plain
-rw-r--r--
rawterm.mli
4427
log
plain
-rwxr-xr-x
recordops.ml
5345
log
plain
-rwxr-xr-x
recordops.mli
1673
log
plain
-rw-r--r--
reductionops.ml
23934
log
plain
-rw-r--r--
reductionops.mli
7507
log
plain
-rw-r--r--
retyping.ml
5100
log
plain
-rw-r--r--
retyping.mli
1408
log
plain
-rw-r--r--
tacred.ml
32171
log
plain
-rw-r--r--
tacred.mli
2926
log
plain
-rw-r--r--
termops.ml
31705
log
plain
-rw-r--r--
termops.mli
7571
log
plain
-rw-r--r--
typing.ml
5254
log
plain
-rw-r--r--
typing.mli
919
log
plain