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
98003
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
17127
log
plain
-rw-r--r--
classops.mli
3687
log
plain
-rw-r--r--
coercion.ml
17979
log
plain
-rw-r--r--
coercion.mli
2941
log
plain
-rw-r--r--
constrMatching.ml
18693
log
plain
-rw-r--r--
constrMatching.mli
4071
log
plain
-rw-r--r--
detyping.ml
33349
log
plain
-rw-r--r--
detyping.mli
3477
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
47977
log
plain
-rw-r--r--
evarconv.mli
2796
log
plain
-rw-r--r--
evarsolve.ml
62141
log
plain
-rw-r--r--
evarsolve.mli
3025
log
plain
-rw-r--r--
evarutil.ml
31186
log
plain
-rw-r--r--
evarutil.mli
9590
log
plain
-rw-r--r--
evd.ml
58854
log
plain
-rw-r--r--
evd.mli
23174
log
plain
-rw-r--r--
find_subterm.ml
6422
log
plain
-rw-r--r--
find_subterm.mli
2907
log
plain
-rw-r--r--
glob_ops.ml
15925
log
plain
-rw-r--r--
glob_ops.mli
2494
log
plain
-rw-r--r--
indrec.ml
21315
log
plain
-rw-r--r--
indrec.mli
2346
log
plain
-rw-r--r--
inductiveops.ml
21424
log
plain
-rw-r--r--
inductiveops.mli
7591
log
plain
-rw-r--r--
locusops.ml
4029
log
plain
-rw-r--r--
locusops.mli
1625
log
plain
-rw-r--r--
miscops.ml
2212
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
14166
log
plain
-rw-r--r--
nativenorm.mli
752
log
plain
-rw-r--r--
patternops.ml
16012
log
plain
-rw-r--r--
patternops.mli
2007
log
plain
-rw-r--r--
pretype_errors.ml
6375
log
plain
-rw-r--r--
pretype_errors.mli
5143
log
plain
-rw-r--r--
pretyping.ml
38499
log
plain
-rw-r--r--
pretyping.mli
5389
log
plain
-rw-r--r--
pretyping.mllib
335
log
plain
-rw-r--r--
program.ml
2703
log
plain
-rw-r--r--
program.mli
1532
log
plain
-rw-r--r--
recordops.ml
11866
log
plain
-rw-r--r--
recordops.mli
2728
log
plain
-rw-r--r--
redops.ml
1521
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
58861
log
plain
-rw-r--r--
reductionops.mli
11510
log
plain
-rw-r--r--
retyping.ml
9737
log
plain
-rw-r--r--
retyping.mli
1961
log
plain
-rw-r--r--
tacred.ml
45809
log
plain
-rw-r--r--
tacred.mli
3922
log
plain
-rw-r--r--
termops.ml
34983
log
plain
-rw-r--r--
termops.mli
10038
log
plain
-rw-r--r--
typeclasses.ml
18560
log
plain
-rw-r--r--
typeclasses.mli
5663
log
plain
-rw-r--r--
typeclasses_errors.ml
1248
log
plain
-rw-r--r--
typeclasses_errors.mli
1131
log
plain
-rw-r--r--
typing.ml
10509
log
plain
-rw-r--r--
typing.mli
1600
log
plain
-rw-r--r--
unification.ml
72691
log
plain
-rw-r--r--
unification.mli
4546
log
plain
-rw-r--r--
vnorm.ml
11186
log
plain
-rw-r--r--
vnorm.mli
629
log
plain