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
3537
log
plain
-rw-r--r--
arguments_renaming.mli
1116
log
plain
-rw-r--r--
cases.ml
106404
log
plain
-rw-r--r--
cases.mli
4665
log
plain
-rw-r--r--
cbv.ml
17864
log
plain
-rw-r--r--
cbv.mli
2325
log
plain
-rw-r--r--
classops.ml
17639
log
plain
-rw-r--r--
classops.mli
3905
log
plain
-rw-r--r--
coercion.ml
19117
log
plain
-rw-r--r--
coercion.mli
3129
log
plain
-rw-r--r--
constr_matching.ml
22097
log
plain
-rw-r--r--
constr_matching.mli
3326
log
plain
-rw-r--r--
constrexpr.ml
6120
log
plain
-rw-r--r--
detyping.ml
41156
log
plain
-rw-r--r--
detyping.mli
4172
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
58145
log
plain
-rw-r--r--
evarconv.mli
3717
log
plain
-rw-r--r--
evardefine.ml
7803
log
plain
-rw-r--r--
evardefine.mli
1966
log
plain
-rw-r--r--
evarsolve.ml
70726
log
plain
-rw-r--r--
evarsolve.mli
3499
log
plain
-rw-r--r--
extend.ml
5010
log
plain
-rw-r--r--
find_subterm.ml
6844
log
plain
-rw-r--r--
find_subterm.mli
3062
log
plain
-rw-r--r--
geninterp.ml
2731
log
plain
-rw-r--r--
geninterp.mli
2480
log
plain
-rw-r--r--
genredexpr.ml
2049
log
plain
-rw-r--r--
glob_ops.ml
21980
log
plain
-rw-r--r--
glob_ops.mli
4260
log
plain
-rw-r--r--
glob_term.ml
5896
log
plain
-rw-r--r--
indrec.ml
23128
log
plain
-rw-r--r--
indrec.mli
2665
log
plain
-rw-r--r--
inductiveops.ml
24380
log
plain
-rw-r--r--
inductiveops.mli
9294
log
plain
-rw-r--r--
inferCumulativity.ml
8256
log
plain
-rw-r--r--
inferCumulativity.mli
780
log
plain
-rw-r--r--
locus.ml
3096
log
plain
-rw-r--r--
locusops.ml
4207
log
plain
-rw-r--r--
locusops.mli
1775
log
plain
-rw-r--r--
ltac_pretype.ml
2556
log
plain
-rw-r--r--
miscops.ml
2858
log
plain
-rw-r--r--
miscops.mli
1424
log
plain
-rw-r--r--
nativenorm.ml
17890
log
plain
-rw-r--r--
nativenorm.mli
1171
log
plain
-rw-r--r--
pattern.ml
2002
log
plain
-rw-r--r--
patternops.ml
21754
log
plain
-rw-r--r--
patternops.mli
2202
log
plain
-rw-r--r--
pretype_errors.ml
6819
log
plain
-rw-r--r--
pretype_errors.mli
5647
log
plain
-rw-r--r--
pretyping.ml
49730
log
plain
-rw-r--r--
pretyping.mli
5324
log
plain
-rw-r--r--
pretyping.mllib
433
log
plain
-rw-r--r--
program.ml
3610
log
plain
-rw-r--r--
program.mli
1748
log
plain
-rw-r--r--
recordops.ml
13894
log
plain
-rw-r--r--
recordops.mli
2975
log
plain
-rw-r--r--
redops.ml
1885
log
plain
-rw-r--r--
redops.mli
784
log
plain
-rw-r--r--
reductionops.ml
62305
log
plain
-rw-r--r--
reductionops.mli
12566
log
plain
-rw-r--r--
retyping.ml
10576
log
plain
-rw-r--r--
retyping.mli
2413
log
plain
-rw-r--r--
tacred.ml
48305
log
plain
-rw-r--r--
tacred.mli
4029
log
plain
-rw-r--r--
typeclasses.ml
19431
log
plain
-rw-r--r--
typeclasses.mli
6311
log
plain
-rw-r--r--
typeclasses_errors.ml
1359
log
plain
-rw-r--r--
typeclasses_errors.mli
1236
log
plain
-rw-r--r--
typing.ml
16675
log
plain
-rw-r--r--
typing.mli
2935
log
plain
-rw-r--r--
unification.ml
77890
log
plain
-rw-r--r--
unification.mli
4466
log
plain
-rw-r--r--
univdecls.ml
2296
log
plain
-rw-r--r--
univdecls.mli
1119
log
plain
-rw-r--r--
vernacexpr.ml
19811
log
plain
-rw-r--r--
vnorm.ml
14926
log
plain
-rw-r--r--
vnorm.mli
797
log
plain