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
3508
log
plain
-rw-r--r--
arguments_renaming.mli
1000
log
plain
-rw-r--r--
cases.ml
95348
log
plain
-rw-r--r--
cases.mli
4237
log
plain
-rw-r--r--
cbv.ml
14069
log
plain
-rw-r--r--
cbv.mli
2073
log
plain
-rw-r--r--
classops.ml
15530
log
plain
-rw-r--r--
classops.mli
3571
log
plain
-rw-r--r--
coercion.ml
16419
log
plain
-rw-r--r--
coercion.mli
2935
log
plain
-rw-r--r--
constrMatching.ml
14691
log
plain
-rw-r--r--
constrMatching.mli
3863
log
plain
-rw-r--r--
detyping.ml
25822
log
plain
-rw-r--r--
detyping.mli
3077
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
37646
log
plain
-rw-r--r--
evarconv.mli
2731
log
plain
-rw-r--r--
evarsolve.ml
56198
log
plain
-rw-r--r--
evarsolve.mli
2574
log
plain
-rw-r--r--
evarutil.ml
27967
log
plain
-rw-r--r--
evarutil.mli
7614
log
plain
-rw-r--r--
evd.ml
32743
log
plain
-rw-r--r--
evd.mli
14134
log
plain
-rw-r--r--
glob_ops.ml
13855
log
plain
-rw-r--r--
glob_ops.mli
1769
log
plain
-rw-r--r--
indrec.ml
19951
log
plain
-rw-r--r--
indrec.mli
2331
log
plain
-rw-r--r--
inductiveops.ml
17635
log
plain
-rw-r--r--
inductiveops.mli
6046
log
plain
-rw-r--r--
locusops.ml
2773
log
plain
-rw-r--r--
locusops.mli
1304
log
plain
-rw-r--r--
miscops.ml
1244
log
plain
-rw-r--r--
miscops.mli
786
log
plain
-rw-r--r--
namegen.ml
11919
log
plain
-rw-r--r--
namegen.mli
3537
log
plain
-rw-r--r--
nativenorm.ml
13029
log
plain
-rw-r--r--
nativenorm.mli
752
log
plain
-rw-r--r--
patternops.ml
15115
log
plain
-rw-r--r--
patternops.mli
1977
log
plain
-rw-r--r--
pretype_errors.ml
5455
log
plain
-rw-r--r--
pretype_errors.mli
4497
log
plain
-rw-r--r--
pretyping.ml
30675
log
plain
-rw-r--r--
pretyping.mli
4704
log
plain
-rw-r--r--
pretyping.mllib
332
log
plain
-rw-r--r--
program.ml
2580
log
plain
-rw-r--r--
program.mli
1229
log
plain
-rw-r--r--
recordops.ml
11580
log
plain
-rw-r--r--
recordops.mli
2690
log
plain
-rw-r--r--
redops.ml
1521
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
44517
log
plain
-rw-r--r--
reductionops.mli
10265
log
plain
-rw-r--r--
retyping.ml
8711
log
plain
-rw-r--r--
retyping.mli
1892
log
plain
-rw-r--r--
tacred.ml
37967
log
plain
-rw-r--r--
tacred.mli
3381
log
plain
-rw-r--r--
term_dnet.ml
12152
log
plain
-rw-r--r--
term_dnet.mli
2610
log
plain
-rw-r--r--
termops.ml
38425
log
plain
-rw-r--r--
termops.mli
11523
log
plain
-rw-r--r--
typeclasses.ml
16574
log
plain
-rw-r--r--
typeclasses.mli
4923
log
plain
-rw-r--r--
typeclasses_errors.ml
1964
log
plain
-rw-r--r--
typeclasses_errors.mli
1535
log
plain
-rw-r--r--
typing.ml
10278
log
plain
-rw-r--r--
typing.mli
1546
log
plain
-rw-r--r--
unification.ml
48973
log
plain
-rw-r--r--
unification.mli
3033
log
plain
-rw-r--r--
vnorm.ml
10591
log
plain
-rw-r--r--
vnorm.mli
629
log
plain