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--
cases.ml
68121
log
plain
-rw-r--r--
cases.mli
1848
log
plain
-rw-r--r--
cbv.ml
13035
log
plain
-rw-r--r--
cbv.mli
1988
log
plain
-rwxr-xr-x
classops.ml
11714
log
plain
-rw-r--r--
classops.mli
3754
log
plain
-rw-r--r--
clenv.ml
14416
log
plain
-rw-r--r--
clenv.mli
4005
log
plain
-rw-r--r--
coercion.ml
6633
log
plain
-rw-r--r--
coercion.mli
1867
log
plain
-rw-r--r--
detyping.ml
18765
log
plain
-rw-r--r--
detyping.mli
1502
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
17076
log
plain
-rw-r--r--
evarconv.mli
1279
log
plain
-rw-r--r--
evarutil.ml
19234
log
plain
-rw-r--r--
evarutil.mli
4372
log
plain
-rw-r--r--
evd.ml
10818
log
plain
-rw-r--r--
evd.mli
5324
log
plain
-rw-r--r--
indrec.ml
19648
log
plain
-rw-r--r--
indrec.mli
1947
log
plain
-rw-r--r--
inductiveops.ml
12387
log
plain
-rw-r--r--
inductiveops.mli
3941
log
plain
-rw-r--r--
matching.ml
9307
log
plain
-rw-r--r--
matching.mli
1994
log
plain
-rw-r--r--
pattern.ml
9705
log
plain
-rw-r--r--
pattern.mli
2641
log
plain
-rw-r--r--
pretype_errors.ml
5850
log
plain
-rw-r--r--
pretype_errors.mli
3299
log
plain
-rw-r--r--
pretyping.ml
42164
log
plain
-rw-r--r--
pretyping.mli
2863
log
plain
-rw-r--r--
rawterm.ml
12720
log
plain
-rw-r--r--
rawterm.mli
4275
log
plain
-rwxr-xr-x
recordops.ml
5330
log
plain
-rwxr-xr-x
recordops.mli
1626
log
plain
-rw-r--r--
reductionops.ml
24416
log
plain
-rw-r--r--
reductionops.mli
7622
log
plain
-rw-r--r--
retyping.ml
5087
log
plain
-rw-r--r--
retyping.mli
1379
log
plain
-rw-r--r--
tacred.ml
32849
log
plain
-rw-r--r--
tacred.mli
3011
log
plain
-rw-r--r--
termops.ml
33729
log
plain
-rw-r--r--
termops.mli
8095
log
plain
-rw-r--r--
typing.ml
5316
log
plain
-rw-r--r--
typing.mli
1327
log
plain
-rw-r--r--
unification.ml
16512
log
plain
-rw-r--r--
unification.mli
1290
log
plain