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
3696
log
plain
-rw-r--r--
arguments_renaming.mli
1000
log
plain
-rw-r--r--
cases.ml
92572
log
plain
-rw-r--r--
cases.mli
3874
log
plain
-rw-r--r--
cbv.ml
14059
log
plain
-rw-r--r--
cbv.mli
2073
log
plain
-rw-r--r--
classops.ml
14220
log
plain
-rw-r--r--
classops.mli
3492
log
plain
-rw-r--r--
coercion.ml
16316
log
plain
-rw-r--r--
coercion.mli
2732
log
plain
-rw-r--r--
detyping.ml
25619
log
plain
-rw-r--r--
detyping.mli
2947
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
35939
log
plain
-rw-r--r--
evarconv.mli
2072
log
plain
-rw-r--r--
evarsolve.ml
56462
log
plain
-rw-r--r--
evarsolve.mli
2366
log
plain
-rw-r--r--
evarutil.ml
27601
log
plain
-rw-r--r--
evarutil.mli
7703
log
plain
-rw-r--r--
evd.ml
30734
log
plain
-rw-r--r--
evd.mli
10981
log
plain
-rw-r--r--
glob_ops.ml
9919
log
plain
-rw-r--r--
glob_ops.mli
1796
log
plain
-rw-r--r--
indrec.ml
19924
log
plain
-rw-r--r--
indrec.mli
2367
log
plain
-rw-r--r--
inductiveops.ml
17530
log
plain
-rw-r--r--
inductiveops.mli
6043
log
plain
-rw-r--r--
locusops.ml
2765
log
plain
-rw-r--r--
locusops.mli
1319
log
plain
-rw-r--r--
matching.ml
13324
log
plain
-rw-r--r--
matching.mli
3957
log
plain
-rw-r--r--
miscops.ml
1974
log
plain
-rw-r--r--
miscops.mli
1003
log
plain
-rw-r--r--
namegen.ml
11857
log
plain
-rw-r--r--
namegen.mli
3524
log
plain
-rw-r--r--
nativenorm.ml
11992
log
plain
-rw-r--r--
nativenorm.mli
699
log
plain
-rw-r--r--
patternops.ml
14978
log
plain
-rw-r--r--
patternops.mli
2034
log
plain
-rw-r--r--
pretype_errors.ml
7259
log
plain
-rw-r--r--
pretype_errors.mli
4526
log
plain
-rw-r--r--
pretyping.ml
28789
log
plain
-rw-r--r--
pretyping.mli
4227
log
plain
-rw-r--r--
pretyping.mllib
326
log
plain
-rw-r--r--
program.ml
2593
log
plain
-rw-r--r--
program.mli
1229
log
plain
-rw-r--r--
recordops.ml
13003
log
plain
-rw-r--r--
recordops.mli
3113
log
plain
-rw-r--r--
redops.ml
1437
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
37216
log
plain
-rw-r--r--
reductionops.mli
9742
log
plain
-rw-r--r--
retyping.ml
7335
log
plain
-rw-r--r--
retyping.mli
1694
log
plain
-rw-r--r--
tacred.ml
40659
log
plain
-rw-r--r--
tacred.mli
3739
log
plain
-rw-r--r--
term_dnet.ml
12953
log
plain
-rw-r--r--
term_dnet.mli
3448
log
plain
-rw-r--r--
termops.ml
38244
log
plain
-rw-r--r--
termops.mli
11133
log
plain
-rw-r--r--
typeclasses.ml
16680
log
plain
-rw-r--r--
typeclasses.mli
4882
log
plain
-rw-r--r--
typeclasses_errors.ml
1891
log
plain
-rw-r--r--
typeclasses_errors.mli
1480
log
plain
-rw-r--r--
typing.ml
10254
log
plain
-rw-r--r--
typing.mli
1546
log
plain
-rw-r--r--
unification.ml
48356
log
plain
-rw-r--r--
unification.mli
2959
log
plain
-rw-r--r--
vnorm.ml
10376
log
plain
-rw-r--r--
vnorm.mli
655
log
plain