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
67964
log
plain
-rw-r--r--
cases.mli
1848
log
plain
-rw-r--r--
cbv.ml
13037
log
plain
-rw-r--r--
cbv.mli
1988
log
plain
-rwxr-xr-x
classops.ml
11654
log
plain
-rw-r--r--
classops.mli
3152
log
plain
-rw-r--r--
clenv.ml
14999
log
plain
-rw-r--r--
clenv.mli
4231
log
plain
-rw-r--r--
coercion.ml
6633
log
plain
-rw-r--r--
coercion.mli
1867
log
plain
-rw-r--r--
detyping.ml
22695
log
plain
-rw-r--r--
detyping.mli
1698
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
17079
log
plain
-rw-r--r--
evarconv.mli
1279
log
plain
-rw-r--r--
evarutil.ml
21854
log
plain
-rw-r--r--
evarutil.mli
4324
log
plain
-rw-r--r--
evd.ml
17127
log
plain
-rw-r--r--
evd.mli
5943
log
plain
-rw-r--r--
indrec.ml
21621
log
plain
-rw-r--r--
indrec.mli
2227
log
plain
-rw-r--r--
inductiveops.ml
13088
log
plain
-rw-r--r--
inductiveops.mli
4385
log
plain
-rw-r--r--
matching.ml
9306
log
plain
-rw-r--r--
matching.mli
1996
log
plain
-rw-r--r--
pattern.ml
9841
log
plain
-rw-r--r--
pattern.mli
2641
log
plain
-rw-r--r--
pretype_errors.ml
5854
log
plain
-rw-r--r--
pretype_errors.mli
3299
log
plain
-rw-r--r--
pretyping.ml
41511
log
plain
-rw-r--r--
pretyping.mli
2856
log
plain
-rw-r--r--
rawterm.ml
8852
log
plain
-rw-r--r--
rawterm.mli
4213
log
plain
-rwxr-xr-x
recordops.ml
8053
log
plain
-rwxr-xr-x
recordops.mli
1866
log
plain
-rw-r--r--
reductionops.ml
26141
log
plain
-rw-r--r--
reductionops.mli
7765
log
plain
-rw-r--r--
retyping.ml
5114
log
plain
-rw-r--r--
retyping.mli
1379
log
plain
-rw-r--r--
tacred.ml
29903
log
plain
-rw-r--r--
tacred.mli
2614
log
plain
-rw-r--r--
termops.ml
33989
log
plain
-rw-r--r--
termops.mli
8202
log
plain
-rw-r--r--
typing.ml
5454
log
plain
-rw-r--r--
typing.mli
1327
log
plain
-rw-r--r--
unification.ml
16550
log
plain
-rw-r--r--
unification.mli
1290
log
plain