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
67146
log
plain
-rw-r--r--
cases.mli
1883
log
plain
-rw-r--r--
cbv.ml
13037
log
plain
-rw-r--r--
cbv.mli
1979
log
plain
-rwxr-xr-x
classops.ml
11821
log
plain
-rw-r--r--
classops.mli
3733
log
plain
-rw-r--r--
coercion.ml
7541
log
plain
-rw-r--r--
coercion.mli
1830
log
plain
-rw-r--r--
detyping.ml
17394
log
plain
-rw-r--r--
detyping.mli
1592
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
14144
log
plain
-rw-r--r--
evarconv.mli
953
log
plain
-rw-r--r--
evarutil.ml
19718
log
plain
-rw-r--r--
evarutil.mli
3244
log
plain
-rw-r--r--
evd.ml
2056
log
plain
-rw-r--r--
evd.mli
1753
log
plain
-rw-r--r--
indrec.ml
21636
log
plain
-rw-r--r--
indrec.mli
1903
log
plain
-rw-r--r--
inductiveops.ml
12028
log
plain
-rw-r--r--
inductiveops.mli
4028
log
plain
-rw-r--r--
instantiate.ml
1957
log
plain
-rw-r--r--
instantiate.mli
946
log
plain
-rw-r--r--
matching.ml
8960
log
plain
-rw-r--r--
matching.mli
1896
log
plain
-rw-r--r--
pattern.ml
10402
log
plain
-rw-r--r--
pattern.mli
2831
log
plain
-rw-r--r--
pretype_errors.ml
5324
log
plain
-rw-r--r--
pretype_errors.mli
2975
log
plain
-rw-r--r--
pretyping.ml
39234
log
plain
-rw-r--r--
pretyping.mli
2667
log
plain
-rw-r--r--
rawterm.ml
10608
log
plain
-rw-r--r--
rawterm.mli
4259
log
plain
-rwxr-xr-x
recordops.ml
5440
log
plain
-rwxr-xr-x
recordops.mli
1802
log
plain
-rw-r--r--
reductionops.ml
24610
log
plain
-rw-r--r--
reductionops.mli
7877
log
plain
-rw-r--r--
retyping.ml
4878
log
plain
-rw-r--r--
retyping.mli
1401
log
plain
-rw-r--r--
tacred.ml
30700
log
plain
-rw-r--r--
tacred.mli
2568
log
plain
-rw-r--r--
termops.ml
27348
log
plain
-rw-r--r--
termops.mli
7196
log
plain
-rw-r--r--
typing.ml
5263
log
plain
-rw-r--r--
typing.mli
912
log
plain