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
3775
log
plain
-rw-r--r--
arguments_renaming.mli
995
log
plain
-rw-r--r--
cases.ml
73369
log
plain
-rw-r--r--
cases.mli
2065
log
plain
-rw-r--r--
cbv.ml
14096
log
plain
-rw-r--r--
cbv.mli
2071
log
plain
-rw-r--r--
classops.ml
13548
log
plain
-rw-r--r--
classops.mli
3419
log
plain
-rw-r--r--
coercion.ml
10504
log
plain
-rw-r--r--
coercion.mli
2897
log
plain
-rw-r--r--
detyping.ml
24968
log
plain
-rw-r--r--
detyping.mli
2866
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
29483
log
plain
-rw-r--r--
evarconv.mli
1951
log
plain
-rw-r--r--
evarutil.ml
69479
log
plain
-rw-r--r--
evarutil.mli
9153
log
plain
-rw-r--r--
evd.ml
29786
log
plain
-rw-r--r--
evd.mli
11287
log
plain
-rw-r--r--
glob_term.ml
14358
log
plain
-rw-r--r--
glob_term.mli
5816
log
plain
-rw-r--r--
indrec.ml
19827
log
plain
-rw-r--r--
indrec.mli
2379
log
plain
-rw-r--r--
inductiveops.ml
16394
log
plain
-rw-r--r--
inductiveops.mli
5397
log
plain
-rw-r--r--
matching.ml
12649
log
plain
-rw-r--r--
matching.mli
3947
log
plain
-rw-r--r--
namegen.ml
11303
log
plain
-rw-r--r--
namegen.mli
3629
log
plain
-rw-r--r--
pattern.ml
13805
log
plain
-rw-r--r--
pattern.mli
4770
log
plain
-rw-r--r--
pretype_errors.ml
6590
log
plain
-rw-r--r--
pretype_errors.mli
4473
log
plain
-rw-r--r--
pretyping.ml
28651
log
plain
-rw-r--r--
pretyping.mli
4402
log
plain
-rw-r--r--
pretyping.mllib
272
log
plain
-rw-r--r--
recordops.ml
12854
log
plain
-rw-r--r--
recordops.mli
3094
log
plain
-rw-r--r--
reductionops.ml
32367
log
plain
-rw-r--r--
reductionops.mli
8979
log
plain
-rw-r--r--
retyping.ml
7270
log
plain
-rw-r--r--
retyping.mli
1694
log
plain
-rw-r--r--
tacred.ml
37800
log
plain
-rw-r--r--
tacred.mli
3644
log
plain
-rw-r--r--
term_dnet.ml
13141
log
plain
-rw-r--r--
term_dnet.mli
3448
log
plain
-rw-r--r--
termops.ml
38200
log
plain
-rw-r--r--
termops.mli
11325
log
plain
-rw-r--r--
typeclasses.ml
15839
log
plain
-rw-r--r--
typeclasses.mli
4471
log
plain
-rw-r--r--
typeclasses_errors.ml
2019
log
plain
-rw-r--r--
typeclasses_errors.mli
1492
log
plain
-rw-r--r--
typing.ml
10084
log
plain
-rw-r--r--
typing.mli
1553
log
plain
-rw-r--r--
unification.ml
45671
log
plain
-rw-r--r--
unification.mli
2858
log
plain
-rw-r--r--
vnorm.ml
10438
log
plain
-rw-r--r--
vnorm.mli
655
log
plain