index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
Mode
Name
Size
-rw-r--r--
arguments_renaming.ml
3544
log
plain
-rw-r--r--
arguments_renaming.mli
1145
log
plain
-rw-r--r--
cases.ml
106219
log
plain
-rw-r--r--
cases.mli
4665
log
plain
-rw-r--r--
cbv.ml
17864
log
plain
-rw-r--r--
cbv.mli
2325
log
plain
-rw-r--r--
classops.ml
17650
log
plain
-rw-r--r--
classops.mli
3922
log
plain
-rw-r--r--
coercion.ml
18840
log
plain
-rw-r--r--
coercion.mli
3129
log
plain
-rw-r--r--
constr_matching.ml
19602
log
plain
-rw-r--r--
constr_matching.mli
3319
log
plain
-rw-r--r--
detyping.ml
40300
log
plain
-rw-r--r--
detyping.mli
3860
log
plain
-rw-r--r--
evarconv.ml
58485
log
plain
-rw-r--r--
evarconv.mli
3438
log
plain
-rw-r--r--
evardefine.ml
7756
log
plain
-rw-r--r--
evardefine.mli
1966
log
plain
-rw-r--r--
evarsolve.ml
71625
log
plain
-rw-r--r--
evarsolve.mli
3499
log
plain
-rw-r--r--
find_subterm.ml
6844
log
plain
-rw-r--r--
find_subterm.mli
3062
log
plain
-rw-r--r--
geninterp.ml
2731
log
plain
-rw-r--r--
geninterp.mli
2480
log
plain
-rw-r--r--
glob_ops.ml
21851
log
plain
-rw-r--r--
glob_ops.mli
4260
log
plain
-rw-r--r--
indrec.ml
23192
log
plain
-rw-r--r--
indrec.mli
2706
log
plain
-rw-r--r--
inductiveops.ml
24376
log
plain
-rw-r--r--
inductiveops.mli
9294
log
plain
-rw-r--r--
inferCumulativity.ml
8278
log
plain
-rw-r--r--
inferCumulativity.mli
780
log
plain
-rw-r--r--
locusops.ml
4207
log
plain
-rw-r--r--
locusops.mli
1775
log
plain
-rw-r--r--
ltac_pretype.ml
2556
log
plain
-rw-r--r--
miscops.ml
2836
log
plain
-rw-r--r--
miscops.mli
1404
log
plain
-rw-r--r--
nativenorm.ml
18395
log
plain
-rw-r--r--
nativenorm.mli
1171
log
plain
-rw-r--r--
patternops.ml
18918
log
plain
-rw-r--r--
patternops.mli
2220
log
plain
-rw-r--r--
pretype_errors.ml
6819
log
plain
-rw-r--r--
pretype_errors.mli
5647
log
plain
-rw-r--r--
pretyping.ml
49474
log
plain
-rw-r--r--
pretyping.mli
5334
log
plain
-rw-r--r--
pretyping.mllib
369
log
plain
-rw-r--r--
program.ml
3574
log
plain
-rw-r--r--
program.mli
1878
log
plain
-rw-r--r--
recordops.ml
13893
log
plain
-rw-r--r--
recordops.mli
3032
log
plain
-rw-r--r--
redops.ml
1885
log
plain
-rw-r--r--
redops.mli
784
log
plain
-rw-r--r--
reductionops.ml
62602
log
plain
-rw-r--r--
reductionops.mli
12634
log
plain
-rw-r--r--
retyping.ml
10624
log
plain
-rw-r--r--
retyping.mli
2413
log
plain
-rw-r--r--
tacred.ml
48278
log
plain
-rw-r--r--
tacred.mli
4109
log
plain
-rw-r--r--
typeclasses.ml
19336
log
plain
-rw-r--r--
typeclasses.mli
6280
log
plain
-rw-r--r--
typeclasses_errors.ml
1370
log
plain
-rw-r--r--
typeclasses_errors.mli
1254
log
plain
-rw-r--r--
typing.ml
15933
log
plain
-rw-r--r--
typing.mli
2476
log
plain
-rw-r--r--
unification.ml
78647
log
plain
-rw-r--r--
unification.mli
4466
log
plain
-rw-r--r--
univdecls.ml
2296
log
plain
-rw-r--r--
univdecls.mli
1119
log
plain
-rw-r--r--
vnorm.ml
15148
log
plain
-rw-r--r--
vnorm.mli
797
log
plain