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
61110
log
plain
-rw-r--r--
cases.mli
1981
log
plain
-rw-r--r--
cbv.ml
13413
log
plain
-rw-r--r--
cbv.mli
2006
log
plain
-rw-r--r--
classops.ml
11637
log
plain
-rw-r--r--
classops.mli
3152
log
plain
-rw-r--r--
clenv.ml
16110
log
plain
-rw-r--r--
clenv.mli
5349
log
plain
-rw-r--r--
coercion.ml
10164
log
plain
-rw-r--r--
coercion.mli
2618
log
plain
-rw-r--r--
detyping.ml
25679
log
plain
-rw-r--r--
detyping.mli
2302
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
19937
log
plain
-rw-r--r--
evarconv.mli
1356
log
plain
-rw-r--r--
evarutil.ml
47091
log
plain
-rw-r--r--
evarutil.mli
6525
log
plain
-rw-r--r--
evd.ml
21025
log
plain
-rw-r--r--
evd.mli
7942
log
plain
-rw-r--r--
indrec.ml
21730
log
plain
-rw-r--r--
indrec.mli
2252
log
plain
-rw-r--r--
inductiveops.ml
14255
log
plain
-rw-r--r--
inductiveops.mli
4859
log
plain
-rw-r--r--
matching.ml
10264
log
plain
-rw-r--r--
matching.mli
1996
log
plain
-rw-r--r--
pattern.ml
11120
log
plain
-rw-r--r--
pattern.mli
2687
log
plain
-rw-r--r--
pretype_errors.ml
6330
log
plain
-rw-r--r--
pretype_errors.mli
3714
log
plain
-rw-r--r--
pretyping.ml
26431
log
plain
-rw-r--r--
pretyping.mli
3744
log
plain
-rw-r--r--
rawterm.ml
12865
log
plain
-rw-r--r--
rawterm.mli
5695
log
plain
-rw-r--r--
recordops.ml
8888
log
plain
-rwxr-xr-x
recordops.mli
1975
log
plain
-rw-r--r--
reductionops.ml
32272
log
plain
-rw-r--r--
reductionops.mli
8609
log
plain
-rw-r--r--
retyping.ml
6042
log
plain
-rw-r--r--
retyping.mli
1497
log
plain
-rw-r--r--
tacred.ml
32060
log
plain
-rw-r--r--
tacred.mli
3043
log
plain
-rw-r--r--
termops.ml
35379
log
plain
-rw-r--r--
termops.mli
9649
log
plain
-rw-r--r--
typeclasses.ml
11102
log
plain
-rw-r--r--
typeclasses.mli
3197
log
plain
-rw-r--r--
typeclasses_errors.ml
1494
log
plain
-rw-r--r--
typeclasses_errors.mli
1388
log
plain
-rw-r--r--
typing.ml
5959
log
plain
-rw-r--r--
typing.mli
1327
log
plain
-rw-r--r--
unification.ml
25545
log
plain
-rw-r--r--
unification.mli
1527
log
plain
-rw-r--r--
vnorm.ml
9641
log
plain
-rw-r--r--
vnorm.mli
662
log
plain