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--
arguments_renaming.ml
3692
log
plain
-rw-r--r--
arguments_renaming.mli
996
log
plain
-rw-r--r--
cases.ml
92569
log
plain
-rw-r--r--
cases.mli
3890
log
plain
-rw-r--r--
cbv.ml
14039
log
plain
-rw-r--r--
cbv.mli
2071
log
plain
-rw-r--r--
classops.ml
13551
log
plain
-rw-r--r--
classops.mli
3420
log
plain
-rw-r--r--
coercion.ml
16054
log
plain
-rw-r--r--
coercion.mli
2732
log
plain
-rw-r--r--
detyping.ml
25198
log
plain
-rw-r--r--
detyping.mli
2975
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
32332
log
plain
-rw-r--r--
evarconv.mli
1968
log
plain
-rw-r--r--
evarutil.ml
79607
log
plain
-rw-r--r--
evarutil.mli
8844
log
plain
-rw-r--r--
evd.ml
29814
log
plain
-rw-r--r--
evd.mli
10784
log
plain
-rw-r--r--
glob_ops.ml
9419
log
plain
-rw-r--r--
glob_ops.mli
1733
log
plain
-rw-r--r--
indrec.ml
19794
log
plain
-rw-r--r--
indrec.mli
2379
log
plain
-rw-r--r--
inductiveops.ml
17266
log
plain
-rw-r--r--
inductiveops.mli
6043
log
plain
-rw-r--r--
locusops.ml
2672
log
plain
-rw-r--r--
locusops.mli
1276
log
plain
-rw-r--r--
matching.ml
12703
log
plain
-rw-r--r--
matching.mli
3947
log
plain
-rw-r--r--
miscops.ml
1862
log
plain
-rw-r--r--
miscops.mli
1003
log
plain
-rw-r--r--
namegen.ml
11659
log
plain
-rw-r--r--
namegen.mli
3658
log
plain
-rw-r--r--
patternops.ml
12788
log
plain
-rw-r--r--
patternops.mli
1980
log
plain
-rw-r--r--
pretype_errors.ml
6537
log
plain
-rw-r--r--
pretype_errors.mli
4487
log
plain
-rw-r--r--
pretyping.ml
28049
log
plain
-rw-r--r--
pretyping.mli
4245
log
plain
-rw-r--r--
pretyping.mllib
305
log
plain
-rw-r--r--
program.ml
2754
log
plain
-rw-r--r--
program.mli
1229
log
plain
-rw-r--r--
recordops.ml
12863
log
plain
-rw-r--r--
recordops.mli
3109
log
plain
-rw-r--r--
redops.ml
1437
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
33142
log
plain
-rw-r--r--
reductionops.mli
9134
log
plain
-rw-r--r--
retyping.ml
7269
log
plain
-rw-r--r--
retyping.mli
1694
log
plain
-rw-r--r--
tacred.ml
39861
log
plain
-rw-r--r--
tacred.mli
3739
log
plain
-rw-r--r--
term_dnet.ml
13123
log
plain
-rw-r--r--
term_dnet.mli
3448
log
plain
-rw-r--r--
termops.ml
38165
log
plain
-rw-r--r--
termops.mli
11153
log
plain
-rw-r--r--
typeclasses.ml
16331
log
plain
-rw-r--r--
typeclasses.mli
4756
log
plain
-rw-r--r--
typeclasses_errors.ml
1966
log
plain
-rw-r--r--
typeclasses_errors.mli
1504
log
plain
-rw-r--r--
typing.ml
10072
log
plain
-rw-r--r--
typing.mli
1553
log
plain
-rw-r--r--
unification.ml
48217
log
plain
-rw-r--r--
unification.mli
2893
log
plain
-rw-r--r--
vnorm.ml
10376
log
plain
-rw-r--r--
vnorm.mli
655
log
plain