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
67585
log
plain
-rw-r--r--
cases.mli
2460
log
plain
-rw-r--r--
cbv.ml
14356
log
plain
-rw-r--r--
cbv.mli
2097
log
plain
-rw-r--r--
classops.ml
12592
log
plain
-rw-r--r--
classops.mli
3403
log
plain
-rw-r--r--
clenv.ml
17238
log
plain
-rw-r--r--
clenv.mli
5534
log
plain
-rw-r--r--
coercion.ml
9774
log
plain
-rw-r--r--
coercion.mli
2923
log
plain
-rw-r--r--
detyping.ml
24926
log
plain
-rw-r--r--
detyping.mli
2301
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
20606
log
plain
-rw-r--r--
evarconv.mli
1574
log
plain
-rw-r--r--
evarutil.ml
52188
log
plain
-rw-r--r--
evarutil.mli
7799
log
plain
-rw-r--r--
evd.ml
26788
log
plain
-rw-r--r--
evd.mli
10184
log
plain
-rw-r--r--
indrec.ml
19574
log
plain
-rw-r--r--
indrec.mli
2398
log
plain
-rw-r--r--
inductiveops.ml
16706
log
plain
-rw-r--r--
inductiveops.mli
5054
log
plain
-rw-r--r--
matching.ml
11309
log
plain
-rw-r--r--
matching.mli
3610
log
plain
-rw-r--r--
pattern.ml
11336
log
plain
-rw-r--r--
pattern.mli
2686
log
plain
-rw-r--r--
pretype_errors.ml
6560
log
plain
-rw-r--r--
pretype_errors.mli
3891
log
plain
-rw-r--r--
pretyping.ml
26309
log
plain
-rw-r--r--
pretyping.mli
3749
log
plain
-rw-r--r--
pretyping.mllib
257
log
plain
-rw-r--r--
rawterm.ml
12777
log
plain
-rw-r--r--
rawterm.mli
5957
log
plain
-rw-r--r--
recordops.ml
11080
log
plain
-rwxr-xr-x
recordops.mli
2915
log
plain
-rw-r--r--
reductionops.ml
32298
log
plain
-rw-r--r--
reductionops.mli
8899
log
plain
-rw-r--r--
retyping.ml
7046
log
plain
-rw-r--r--
retyping.mli
1523
log
plain
-rw-r--r--
tacred.ml
33845
log
plain
-rw-r--r--
tacred.mli
3287
log
plain
-rw-r--r--
term_dnet.ml
12639
log
plain
-rw-r--r--
term_dnet.mli
3458
log
plain
-rw-r--r--
termops.ml
32838
log
plain
-rw-r--r--
termops.mli
9796
log
plain
-rw-r--r--
typeclasses.ml
11861
log
plain
-rw-r--r--
typeclasses.mli
3552
log
plain
-rw-r--r--
typeclasses_errors.ml
2026
log
plain
-rw-r--r--
typeclasses_errors.mli
1518
log
plain
-rw-r--r--
typing.ml
5862
log
plain
-rw-r--r--
typing.mli
1325
log
plain
-rw-r--r--
unification.ml
36098
log
plain
-rw-r--r--
unification.mli
2037
log
plain
-rw-r--r--
vnorm.ml
10428
log
plain
-rw-r--r--
vnorm.mli
662
log
plain