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
3787
log
plain
-rw-r--r--
arguments_renaming.mli
995
log
plain
-rw-r--r--
cases.ml
92610
log
plain
-rw-r--r--
cases.mli
3884
log
plain
-rw-r--r--
cbv.ml
14108
log
plain
-rw-r--r--
cbv.mli
2071
log
plain
-rw-r--r--
classops.ml
13557
log
plain
-rw-r--r--
classops.mli
3419
log
plain
-rw-r--r--
coercion.ml
16109
log
plain
-rw-r--r--
coercion.mli
2728
log
plain
-rw-r--r--
detyping.ml
25064
log
plain
-rw-r--r--
detyping.mli
2878
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
32151
log
plain
-rw-r--r--
evarconv.mli
1962
log
plain
-rw-r--r--
evarutil.ml
79092
log
plain
-rw-r--r--
evarutil.mli
8911
log
plain
-rw-r--r--
evd.ml
29819
log
plain
-rw-r--r--
evd.mli
10795
log
plain
-rw-r--r--
glob_ops.ml
9498
log
plain
-rw-r--r--
glob_ops.mli
1749
log
plain
-rw-r--r--
indrec.ml
19846
log
plain
-rw-r--r--
indrec.mli
2379
log
plain
-rw-r--r--
inductiveops.ml
17284
log
plain
-rw-r--r--
inductiveops.mli
6043
log
plain
-rw-r--r--
locusops.ml
2698
log
plain
-rw-r--r--
locusops.mli
1276
log
plain
-rw-r--r--
matching.ml
12724
log
plain
-rw-r--r--
matching.mli
3947
log
plain
-rw-r--r--
miscops.ml
1862
log
plain
-rw-r--r--
miscops.mli
1002
log
plain
-rw-r--r--
namegen.ml
11664
log
plain
-rw-r--r--
namegen.mli
3658
log
plain
-rw-r--r--
pattern.ml
13908
log
plain
-rw-r--r--
pattern.mli
4777
log
plain
-rw-r--r--
pretype_errors.ml
6604
log
plain
-rw-r--r--
pretype_errors.mli
4481
log
plain
-rw-r--r--
pretyping.ml
27390
log
plain
-rw-r--r--
pretyping.mli
4246
log
plain
-rw-r--r--
pretyping.mllib
303
log
plain
-rw-r--r--
program.ml
2918
log
plain
-rw-r--r--
recordops.ml
12866
log
plain
-rw-r--r--
recordops.mli
3094
log
plain
-rw-r--r--
redops.ml
1437
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
32448
log
plain
-rw-r--r--
reductionops.mli
9026
log
plain
-rw-r--r--
retyping.ml
7282
log
plain
-rw-r--r--
retyping.mli
1694
log
plain
-rw-r--r--
tacred.ml
38379
log
plain
-rw-r--r--
tacred.mli
3735
log
plain
-rw-r--r--
term_dnet.ml
13148
log
plain
-rw-r--r--
term_dnet.mli
3448
log
plain
-rw-r--r--
termops.ml
38214
log
plain
-rw-r--r--
termops.mli
11165
log
plain
-rw-r--r--
typeclasses.ml
16148
log
plain
-rw-r--r--
typeclasses.mli
4575
log
plain
-rw-r--r--
typeclasses_errors.ml
2030
log
plain
-rw-r--r--
typeclasses_errors.mli
1505
log
plain
-rw-r--r--
typing.ml
10096
log
plain
-rw-r--r--
typing.mli
1553
log
plain
-rw-r--r--
unification.ml
47405
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