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
62298
log
plain
-rw-r--r--
cases.mli
1622
log
plain
-rw-r--r--
cbv.ml
13413
log
plain
-rw-r--r--
cbv.mli
2006
log
plain
-rw-r--r--
classops.ml
11581
log
plain
-rw-r--r--
classops.mli
3152
log
plain
-rw-r--r--
clenv.ml
15023
log
plain
-rw-r--r--
clenv.mli
4231
log
plain
-rw-r--r--
coercion.ml
10325
log
plain
-rw-r--r--
coercion.mli
2618
log
plain
-rw-r--r--
detyping.ml
23693
log
plain
-rw-r--r--
detyping.mli
2201
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
19865
log
plain
-rw-r--r--
evarconv.mli
1356
log
plain
-rw-r--r--
evarutil.ml
27140
log
plain
-rw-r--r--
evarutil.mli
5957
log
plain
-rw-r--r--
evd.ml
17336
log
plain
-rw-r--r--
evd.mli
6002
log
plain
-rw-r--r--
indrec.ml
21632
log
plain
-rw-r--r--
indrec.mli
2227
log
plain
-rw-r--r--
inductiveops.ml
14895
log
plain
-rw-r--r--
inductiveops.mli
4802
log
plain
-rw-r--r--
matching.ml
10185
log
plain
-rw-r--r--
matching.mli
1996
log
plain
-rw-r--r--
pattern.ml
11089
log
plain
-rw-r--r--
pattern.mli
2687
log
plain
-rw-r--r--
pretype_errors.ml
6077
log
plain
-rw-r--r--
pretype_errors.mli
3453
log
plain
-rw-r--r--
pretyping.ml
25158
log
plain
-rw-r--r--
pretyping.mli
3584
log
plain
-rw-r--r--
rawterm.ml
10001
log
plain
-rw-r--r--
rawterm.mli
4980
log
plain
-rw-r--r--
recordops.ml
8282
log
plain
-rwxr-xr-x
recordops.mli
1769
log
plain
-rw-r--r--
reductionops.ml
29017
log
plain
-rw-r--r--
reductionops.mli
8474
log
plain
-rw-r--r--
retyping.ml
5798
log
plain
-rw-r--r--
retyping.mli
1491
log
plain
-rw-r--r--
tacred.ml
30136
log
plain
-rw-r--r--
tacred.mli
2775
log
plain
-rw-r--r--
termops.ml
34213
log
plain
-rw-r--r--
termops.mli
8246
log
plain
-rw-r--r--
typing.ml
5458
log
plain
-rw-r--r--
typing.mli
1327
log
plain
-rw-r--r--
unification.ml
17315
log
plain
-rw-r--r--
unification.mli
1290
log
plain
-rw-r--r--
vnorm.ml
9082
log
plain
-rw-r--r--
vnorm.mli
662
log
plain