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
3611
log
plain
-rw-r--r--
arguments_renaming.mli
1003
log
plain
-rw-r--r--
cases.ml
98529
log
plain
-rw-r--r--
cases.mli
4209
log
plain
-rw-r--r--
cbv.ml
15116
log
plain
-rw-r--r--
cbv.mli
2150
log
plain
-rw-r--r--
classops.ml
17112
log
plain
-rw-r--r--
classops.mli
3687
log
plain
-rw-r--r--
coercion.ml
17704
log
plain
-rw-r--r--
coercion.mli
2941
log
plain
-rw-r--r--
constr_matching.ml
18184
log
plain
-rw-r--r--
constr_matching.mli
4071
log
plain
-rw-r--r--
detyping.ml
33410
log
plain
-rw-r--r--
detyping.mli
3513
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
49366
log
plain
-rw-r--r--
evarconv.mli
3010
log
plain
-rw-r--r--
evarsolve.ml
62981
log
plain
-rw-r--r--
evarsolve.mli
3025
log
plain
-rw-r--r--
evarutil.ml
32286
log
plain
-rw-r--r--
evarutil.mli
10497
log
plain
-rw-r--r--
evd.ml
58810
log
plain
-rw-r--r--
evd.mli
22816
log
plain
-rw-r--r--
find_subterm.ml
6409
log
plain
-rw-r--r--
find_subterm.mli
2896
log
plain
-rw-r--r--
glob_ops.ml
15925
log
plain
-rw-r--r--
glob_ops.mli
2595
log
plain
-rw-r--r--
indrec.ml
21315
log
plain
-rw-r--r--
indrec.mli
2346
log
plain
-rw-r--r--
inductiveops.ml
21504
log
plain
-rw-r--r--
inductiveops.mli
7953
log
plain
-rw-r--r--
locusops.ml
4029
log
plain
-rw-r--r--
locusops.mli
1625
log
plain
-rw-r--r--
miscops.ml
2244
log
plain
-rw-r--r--
miscops.mli
1093
log
plain
-rw-r--r--
namegen.ml
14019
log
plain
-rw-r--r--
namegen.mli
4215
log
plain
-rw-r--r--
nativenorm.ml
14115
log
plain
-rw-r--r--
nativenorm.mli
752
log
plain
-rw-r--r--
patternops.ml
16694
log
plain
-rw-r--r--
patternops.mli
2025
log
plain
-rw-r--r--
pretype_errors.ml
6420
log
plain
-rw-r--r--
pretype_errors.mli
5179
log
plain
-rw-r--r--
pretyping.ml
38450
log
plain
-rw-r--r--
pretyping.mli
5391
log
plain
-rw-r--r--
pretyping.mllib
336
log
plain
-rw-r--r--
program.ml
2703
log
plain
-rw-r--r--
program.mli
1532
log
plain
-rw-r--r--
recordops.ml
12009
log
plain
-rw-r--r--
recordops.mli
2889
log
plain
-rw-r--r--
redops.ml
1521
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
59877
log
plain
-rw-r--r--
reductionops.mli
11718
log
plain
-rw-r--r--
retyping.ml
9824
log
plain
-rw-r--r--
retyping.mli
1961
log
plain
-rw-r--r--
tacred.ml
45655
log
plain
-rw-r--r--
tacred.mli
3922
log
plain
-rw-r--r--
termops.ml
35007
log
plain
-rw-r--r--
termops.mli
10027
log
plain
-rw-r--r--
typeclasses.ml
18326
log
plain
-rw-r--r--
typeclasses.mli
5619
log
plain
-rw-r--r--
typeclasses_errors.ml
1239
log
plain
-rw-r--r--
typeclasses_errors.mli
1122
log
plain
-rw-r--r--
typing.ml
10509
log
plain
-rw-r--r--
typing.mli
1589
log
plain
-rw-r--r--
unification.ml
73269
log
plain
-rw-r--r--
unification.mli
4546
log
plain
-rw-r--r--
vnorm.ml
11348
log
plain
-rw-r--r--
vnorm.mli
629
log
plain