index
:
debian-coq
master
pristine-tar
upstream
Debian packaging for Coq
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
contrib
/
correctness
Mode
Name
Size
-rw-r--r--
ArrayPermut.v
5639
log
plain
-rw-r--r--
Arrays.v
2378
log
plain
-rw-r--r--
Arrays_stuff.v
739
log
plain
-rw-r--r--
Correctness.v
867
log
plain
-rw-r--r--
Exchange.v
2999
log
plain
-rw-r--r--
ProgBool.v
1983
log
plain
-rw-r--r--
ProgInt.v
810
log
plain
-rw-r--r--
ProgramsExtraction.v
1199
log
plain
-rw-r--r--
Programs_stuff.v
693
log
plain
-rw-r--r--
Sorted.v
5254
log
plain
-rw-r--r--
Tuples.v
3324
log
plain
d---------
examples
217
log
plain
-rw-r--r--
past.mli
2959
log
plain
-rw-r--r--
pcic.ml
7249
log
plain
-rw-r--r--
pcic.mli
941
log
plain
-rw-r--r--
pcicenv.ml
3464
log
plain
-rw-r--r--
pcicenv.mli
1577
log
plain
-rw-r--r--
pdb.ml
4716
log
plain
-rw-r--r--
pdb.mli
994
log
plain
-rw-r--r--
peffect.ml
3806
log
plain
-rw-r--r--
peffect.mli
1271
log
plain
-rw-r--r--
penv.ml
6436
log
plain
-rw-r--r--
penv.mli
2815
log
plain
-rw-r--r--
perror.ml
5566
log
plain
-rw-r--r--
perror.mli
1709
log
plain
-rw-r--r--
pextract.ml
14654
log
plain
-rw-r--r--
pextract.mli
704
log
plain
-rw-r--r--
pmisc.ml
6342
log
plain
-rw-r--r--
pmisc.mli
2684
log
plain
-rw-r--r--
pmlize.ml
10235
log
plain
-rw-r--r--
pmlize.mli
821
log
plain
-rw-r--r--
pmonad.ml
20834
log
plain
-rw-r--r--
pmonad.mli
3541
log
plain
-rw-r--r--
pred.ml
3549
log
plain
-rw-r--r--
pred.mli
900
log
plain
-rw-r--r--
prename.ml
3751
log
plain
-rw-r--r--
prename.mli
2037
log
plain
-rw-r--r--
preuves.v
2711
log
plain
-rw-r--r--
psyntax.ml4
31093
log
plain
-rw-r--r--
psyntax.mli
940
log
plain
-rw-r--r--
ptactic.ml
8376
log
plain
-rw-r--r--
ptactic.mli
1085
log
plain
-rw-r--r--
ptype.mli
2190
log
plain
-rw-r--r--
ptyping.ml
19457
log
plain
-rw-r--r--
ptyping.mli
1334
log
plain
-rw-r--r--
putil.ml
9034
log
plain
-rw-r--r--
putil.mli
2682
log
plain
-rw-r--r--
pwp.ml
11115
log
plain
-rw-r--r--
pwp.mli
808
log
plain