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
98161
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
17704
log
plain
-rw-r--r--
coercion.mli
2941
log
plain
-rw-r--r--
constr_matching.ml
18672
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
49515
log
plain
-rw-r--r--
evarconv.mli
3010
log
plain
-rw-r--r--
evarsolve.ml
61582
log
plain
-rw-r--r--
evarsolve.mli
3025
log
plain
-rw-r--r--
evarutil.ml
31257
log
plain
-rw-r--r--
evarutil.mli
9686
log
plain
-rw-r--r--
evd.ml
59401
log
plain
-rw-r--r--
evd.mli
23233
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
2494
log
plain
-rw-r--r--
indrec.ml
21315
log
plain
-rw-r--r--
indrec.mli
2346
log
plain
-rw-r--r--
inductiveops.ml
21409
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
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
16012
log
plain
-rw-r--r--
patternops.mli
2007
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
38451
log
plain
-rw-r--r--
pretyping.mli
5389
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
59205
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
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
72769
log
plain
-rw-r--r--
unification.mli
4546
log
plain
-rw-r--r--
vnorm.ml
11089
log
plain
-rw-r--r--
vnorm.mli
629
log
plain