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
3628
log
plain
-rw-r--r--
arguments_renaming.mli
993
log
plain
-rw-r--r--
cases.ml
101396
log
plain
-rw-r--r--
cases.mli
4271
log
plain
-rw-r--r--
cbv.ml
15180
log
plain
-rw-r--r--
cbv.mli
2159
log
plain
-rw-r--r--
classops.ml
17366
log
plain
-rw-r--r--
classops.mli
3781
log
plain
-rw-r--r--
coercion.ml
18596
log
plain
-rw-r--r--
coercion.mli
2941
log
plain
-rw-r--r--
constr_matching.ml
18724
log
plain
-rw-r--r--
constr_matching.mli
4154
log
plain
-rw-r--r--
detyping.ml
35161
log
plain
-rw-r--r--
detyping.mli
3502
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
54857
log
plain
-rw-r--r--
evarconv.mli
2996
log
plain
-rw-r--r--
evardefine.ml
8471
log
plain
-rw-r--r--
evardefine.mli
1875
log
plain
-rw-r--r--
evarsolve.ml
67859
log
plain
-rw-r--r--
evarsolve.mli
3207
log
plain
-rw-r--r--
find_subterm.ml
6871
log
plain
-rw-r--r--
find_subterm.mli
2987
log
plain
-rw-r--r--
glob_ops.ml
21427
log
plain
-rw-r--r--
glob_ops.mli
3191
log
plain
-rw-r--r--
indrec.ml
21903
log
plain
-rw-r--r--
indrec.mli
2537
log
plain
-rw-r--r--
inductiveops.ml
23333
log
plain
-rw-r--r--
inductiveops.mli
8796
log
plain
-rw-r--r--
locusops.ml
4032
log
plain
-rw-r--r--
locusops.mli
1625
log
plain
-rw-r--r--
miscops.ml
2270
log
plain
-rw-r--r--
miscops.mli
1093
log
plain
-rw-r--r--
nativenorm.ml
14996
log
plain
-rw-r--r--
nativenorm.mli
854
log
plain
-rw-r--r--
patternops.ml
16222
log
plain
-rw-r--r--
patternops.mli
1978
log
plain
-rw-r--r--
pretype_errors.ml
6338
log
plain
-rw-r--r--
pretype_errors.mli
5160
log
plain
-rw-r--r--
pretyping.ml
47361
log
plain
-rw-r--r--
pretyping.mli
6271
log
plain
-rw-r--r--
pretyping.mllib
318
log
plain
-rw-r--r--
program.ml
3916
log
plain
-rw-r--r--
program.mli
1663
log
plain
-rw-r--r--
recordops.ml
12594
log
plain
-rw-r--r--
recordops.mli
2885
log
plain
-rw-r--r--
redops.ml
1711
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
62871
log
plain
-rw-r--r--
reductionops.mli
12206
log
plain
-rw-r--r--
retyping.ml
11009
log
plain
-rw-r--r--
retyping.mli
2094
log
plain
-rw-r--r--
tacred.ml
49022
log
plain
-rw-r--r--
tacred.mli
3893
log
plain
-rw-r--r--
typeclasses.ml
18565
log
plain
-rw-r--r--
typeclasses.mli
5628
log
plain
-rw-r--r--
typeclasses_errors.ml
1228
log
plain
-rw-r--r--
typeclasses_errors.mli
1113
log
plain
-rw-r--r--
typing.ml
12009
log
plain
-rw-r--r--
typing.mli
1994
log
plain
-rw-r--r--
unification.ml
78397
log
plain
-rw-r--r--
unification.mli
4595
log
plain
-rw-r--r--
vnorm.ml
13536
log
plain
-rw-r--r--
vnorm.mli
649
log
plain