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
57178
log
plain
-rw-r--r--
cases.mli
1577
log
plain
-rw-r--r--
cbv.ml
14667
log
plain
-rw-r--r--
cbv.mli
2268
log
plain
-rwxr-xr-x
classops.ml
9458
log
plain
-rw-r--r--
classops.mli
3821
log
plain
-rw-r--r--
coercion.ml
7116
log
plain
-rw-r--r--
coercion.mli
1876
log
plain
-rw-r--r--
detyping.ml
11505
log
plain
-rw-r--r--
detyping.mli
1188
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
12597
log
plain
-rw-r--r--
evarconv.mli
953
log
plain
-rw-r--r--
evarutil.ml
18278
log
plain
-rw-r--r--
evarutil.mli
3000
log
plain
-rw-r--r--
evd.ml
1991
log
plain
-rw-r--r--
evd.mli
1704
log
plain
-rw-r--r--
indrec.ml
20253
log
plain
-rw-r--r--
indrec.mli
1840
log
plain
-rw-r--r--
inductiveops.ml
13082
log
plain
-rw-r--r--
inductiveops.mli
3250
log
plain
-rw-r--r--
instantiate.ml
1857
log
plain
-rw-r--r--
instantiate.mli
946
log
plain
-rw-r--r--
multcase.mli
901
log
plain
-rw-r--r--
pattern.ml
11818
log
plain
-rw-r--r--
pattern.mli
3296
log
plain
-rw-r--r--
pretype_errors.ml
5375
log
plain
-rw-r--r--
pretype_errors.mli
3055
log
plain
-rw-r--r--
pretyping.ml
20080
log
plain
-rw-r--r--
pretyping.mli
2697
log
plain
-rw-r--r--
rawterm.ml
3756
log
plain
-rw-r--r--
rawterm.mli
2608
log
plain
-rwxr-xr-x
recordops.ml
3631
log
plain
-rwxr-xr-x
recordops.mli
1699
log
plain
-rw-r--r--
reductionops.ml
23906
log
plain
-rw-r--r--
reductionops.mli
7716
log
plain
-rw-r--r--
retyping.ml
4932
log
plain
-rw-r--r--
retyping.mli
1411
log
plain
-rw-r--r--
syntax_def.ml
2242
log
plain
-rw-r--r--
syntax_def.mli
796
log
plain
-rw-r--r--
tacred.ml
27352
log
plain
-rw-r--r--
tacred.mli
2358
log
plain
-rw-r--r--
termops.ml
23699
log
plain
-rw-r--r--
termops.mli
5993
log
plain
-rw-r--r--
typing.ml
5110
log
plain
-rw-r--r--
typing.mli
912
log
plain