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
91720
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
13463
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
25269
log
plain
-rw-r--r--
detyping.mli
2975
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
32216
log
plain
-rw-r--r--
evarconv.mli
1968
log
plain
-rw-r--r--
evarutil.ml
79331
log
plain
-rw-r--r--
evarutil.mli
8844
log
plain
-rw-r--r--
evd.ml
29707
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
17273
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
12784
log
plain
-rw-r--r--
matching.mli
3969
log
plain
-rw-r--r--
miscops.ml
1862
log
plain
-rw-r--r--
miscops.mli
1003
log
plain
-rw-r--r--
namegen.ml
11662
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
6718
log
plain
-rw-r--r--
pretype_errors.mli
4650
log
plain
-rw-r--r--
pretyping.ml
27902
log
plain
-rw-r--r--
pretyping.mli
4245
log
plain
-rw-r--r--
pretyping.mllib
305
log
plain
-rw-r--r--
program.ml
2573
log
plain
-rw-r--r--
program.mli
1229
log
plain
-rw-r--r--
recordops.ml
12879
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
33124
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
39863
log
plain
-rw-r--r--
tacred.mli
3739
log
plain
-rw-r--r--
term_dnet.ml
12903
log
plain
-rw-r--r--
term_dnet.mli
3448
log
plain
-rw-r--r--
termops.ml
38439
log
plain
-rw-r--r--
termops.mli
11276
log
plain
-rw-r--r--
typeclasses.ml
16126
log
plain
-rw-r--r--
typeclasses.mli
4756
log
plain
-rw-r--r--
typeclasses_errors.ml
1956
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
48303
log
plain
-rw-r--r--
unification.mli
2901
log
plain
-rw-r--r--
vnorm.ml
10376
log
plain
-rw-r--r--
vnorm.mli
655
log
plain