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
3633
log
plain
-rw-r--r--
arguments_renaming.mli
995
log
plain
-rw-r--r--
cases.ml
106109
log
plain
-rw-r--r--
cases.mli
4515
log
plain
-rw-r--r--
cbv.ml
17612
log
plain
-rw-r--r--
cbv.mli
2173
log
plain
-rw-r--r--
classops.ml
17500
log
plain
-rw-r--r--
classops.mli
3772
log
plain
-rw-r--r--
coercion.ml
18690
log
plain
-rw-r--r--
coercion.mli
2979
log
plain
-rw-r--r--
constr_matching.ml
19141
log
plain
-rw-r--r--
constr_matching.mli
3169
log
plain
-rw-r--r--
detyping.ml
40021
log
plain
-rw-r--r--
detyping.mli
3710
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
59870
log
plain
-rw-r--r--
evarconv.mli
3284
log
plain
-rw-r--r--
evardefine.ml
7598
log
plain
-rw-r--r--
evardefine.mli
1816
log
plain
-rw-r--r--
evarsolve.ml
71462
log
plain
-rw-r--r--
evarsolve.mli
3345
log
plain
-rw-r--r--
find_subterm.ml
6694
log
plain
-rw-r--r--
find_subterm.mli
2912
log
plain
-rw-r--r--
geninterp.ml
2581
log
plain
-rw-r--r--
geninterp.mli
2330
log
plain
-rw-r--r--
glob_ops.ml
20610
log
plain
-rw-r--r--
glob_ops.mli
3765
log
plain
-rw-r--r--
indrec.ml
22968
log
plain
-rw-r--r--
indrec.mli
2532
log
plain
-rw-r--r--
inductiveops.ml
27750
log
plain
-rw-r--r--
inductiveops.mli
9558
log
plain
-rw-r--r--
locusops.ml
4057
log
plain
-rw-r--r--
locusops.mli
1625
log
plain
-rw-r--r--
ltac_pretype.ml
2556
log
plain
-rw-r--r--
miscops.ml
2682
log
plain
-rw-r--r--
miscops.mli
1254
log
plain
-rw-r--r--
nativenorm.ml
17241
log
plain
-rw-r--r--
nativenorm.mli
1021
log
plain
-rw-r--r--
patternops.ml
18714
log
plain
-rw-r--r--
patternops.mli
2070
log
plain
-rw-r--r--
pretype_errors.ml
6669
log
plain
-rw-r--r--
pretype_errors.mli
5497
log
plain
-rw-r--r--
pretyping.ml
49304
log
plain
-rw-r--r--
pretyping.mli
4888
log
plain
-rw-r--r--
pretyping.mllib
351
log
plain
-rw-r--r--
program.ml
3424
log
plain
-rw-r--r--
program.mli
1728
log
plain
-rw-r--r--
recordops.ml
13254
log
plain
-rw-r--r--
recordops.mli
2882
log
plain
-rw-r--r--
redops.ml
1735
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
64924
log
plain
-rw-r--r--
reductionops.mli
12690
log
plain
-rw-r--r--
retyping.ml
10474
log
plain
-rw-r--r--
retyping.mli
2261
log
plain
-rw-r--r--
tacred.ml
48187
log
plain
-rw-r--r--
tacred.mli
3959
log
plain
-rw-r--r--
typeclasses.ml
19244
log
plain
-rw-r--r--
typeclasses.mli
6034
log
plain
-rw-r--r--
typeclasses_errors.ml
1231
log
plain
-rw-r--r--
typeclasses_errors.mli
1116
log
plain
-rw-r--r--
typing.ml
14727
log
plain
-rw-r--r--
typing.mli
2326
log
plain
-rw-r--r--
unification.ml
79307
log
plain
-rw-r--r--
unification.mli
4316
log
plain
-rw-r--r--
univdecls.ml
2129
log
plain
-rw-r--r--
univdecls.mli
975
log
plain
-rw-r--r--
vnorm.ml
13686
log
plain
-rw-r--r--
vnorm.mli
647
log
plain