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
3628
log
plain
-rw-r--r--
arguments_renaming.mli
993
log
plain
-rw-r--r--
cases.ml
103141
log
plain
-rw-r--r--
cases.mli
4204
log
plain
-rw-r--r--
cbv.ml
15200
log
plain
-rw-r--r--
cbv.mli
2176
log
plain
-rw-r--r--
classops.ml
17425
log
plain
-rw-r--r--
classops.mli
3785
log
plain
-rw-r--r--
coercion.ml
18614
log
plain
-rw-r--r--
coercion.mli
2954
log
plain
-rw-r--r--
constr_matching.ml
19243
log
plain
-rw-r--r--
constr_matching.mli
4170
log
plain
-rw-r--r--
detyping.ml
35630
log
plain
-rw-r--r--
detyping.mli
3537
log
plain
-rw-r--r--
doc.tex
215
log
plain
-rw-r--r--
evarconv.ml
54609
log
plain
-rw-r--r--
evarconv.mli
3168
log
plain
-rw-r--r--
evardefine.ml
8107
log
plain
-rw-r--r--
evardefine.mli
1828
log
plain
-rw-r--r--
evarsolve.ml
71281
log
plain
-rw-r--r--
evarsolve.mli
3382
log
plain
-rw-r--r--
find_subterm.ml
6704
log
plain
-rw-r--r--
find_subterm.mli
2922
log
plain
-rw-r--r--
glob_ops.ml
21822
log
plain
-rw-r--r--
glob_ops.mli
3191
log
plain
-rw-r--r--
indrec.ml
23150
log
plain
-rw-r--r--
indrec.mli
2537
log
plain
-rw-r--r--
inductiveops.ml
24020
log
plain
-rw-r--r--
inductiveops.mli
9093
log
plain
-rw-r--r--
locusops.ml
4032
log
plain
-rw-r--r--
locusops.mli
1625
log
plain
-rw-r--r--
miscops.ml
2639
log
plain
-rw-r--r--
miscops.mli
1254
log
plain
-rw-r--r--
nativenorm.ml
15048
log
plain
-rw-r--r--
nativenorm.mli
852
log
plain
-rw-r--r--
patternops.ml
16455
log
plain
-rw-r--r--
patternops.mli
2009
log
plain
-rw-r--r--
pretype_errors.ml
6743
log
plain
-rw-r--r--
pretype_errors.mli
5569
log
plain
-rw-r--r--
pretyping.ml
49037
log
plain
-rw-r--r--
pretyping.mli
6307
log
plain
-rw-r--r--
pretyping.mllib
318
log
plain
-rw-r--r--
program.ml
4002
log
plain
-rw-r--r--
program.mli
1666
log
plain
-rw-r--r--
recordops.ml
12701
log
plain
-rw-r--r--
recordops.mli
2869
log
plain
-rw-r--r--
redops.ml
1711
log
plain
-rw-r--r--
redops.mli
634
log
plain
-rw-r--r--
reductionops.ml
61821
log
plain
-rw-r--r--
reductionops.mli
12069
log
plain
-rw-r--r--
retyping.ml
10606
log
plain
-rw-r--r--
retyping.mli
2017
log
plain
-rw-r--r--
tacred.ml
47875
log
plain
-rw-r--r--
tacred.mli
3951
log
plain
-rw-r--r--
typeclasses.ml
18748
log
plain
-rw-r--r--
typeclasses.mli
5860
log
plain
-rw-r--r--
typeclasses_errors.ml
1241
log
plain
-rw-r--r--
typeclasses_errors.mli
1126
log
plain
-rw-r--r--
typing.ml
15210
log
plain
-rw-r--r--
typing.mli
2317
log
plain
-rw-r--r--
unification.ml
79586
log
plain
-rw-r--r--
unification.mli
4330
log
plain
-rw-r--r--
vnorm.ml
13674
log
plain
-rw-r--r--
vnorm.mli
647
log
plain