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
5647
log
plain
-rw-r--r--
Arrays.v
2386
log
plain
-rw-r--r--
Arrays_stuff.v
748
log
plain
-rw-r--r--
Correctness.v
875
log
plain
-rw-r--r--
Exchange.v
3007
log
plain
-rw-r--r--
ProgBool.v
1991
log
plain
-rw-r--r--
ProgInt.v
818
log
plain
-rw-r--r--
ProgramsExtraction.v
1208
log
plain
-rw-r--r--
Programs_stuff.v
702
log
plain
-rw-r--r--
Sorted.v
5262
log
plain
-rw-r--r--
Tuples.v
3332
log
plain
d---------
examples
217
log
plain
-rw-r--r--
past.mli
2967
log
plain
-rw-r--r--
pcic.ml
7258
log
plain
-rw-r--r--
pcic.mli
950
log
plain
-rw-r--r--
pcicenv.ml
3473
log
plain
-rw-r--r--
pcicenv.mli
1586
log
plain
-rw-r--r--
pdb.ml
4724
log
plain
-rw-r--r--
pdb.mli
1003
log
plain
-rw-r--r--
peffect.ml
3815
log
plain
-rw-r--r--
peffect.mli
1280
log
plain
-rw-r--r--
penv.ml
6445
log
plain
-rw-r--r--
penv.mli
2823
log
plain
-rw-r--r--
perror.ml
5574
log
plain
-rw-r--r--
perror.mli
1717
log
plain
-rw-r--r--
pextract.ml
14662
log
plain
-rw-r--r--
pextract.mli
713
log
plain
-rw-r--r--
pmisc.ml
6351
log
plain
-rw-r--r--
pmisc.mli
2692
log
plain
-rw-r--r--
pmlize.ml
10243
log
plain
-rw-r--r--
pmlize.mli
830
log
plain
-rw-r--r--
pmonad.ml
20843
log
plain
-rw-r--r--
pmonad.mli
3550
log
plain
-rw-r--r--
pred.ml
3558
log
plain
-rw-r--r--
pred.mli
909
log
plain
-rw-r--r--
prename.ml
3760
log
plain
-rw-r--r--
prename.mli
2046
log
plain
-rw-r--r--
preuves.v
2711
log
plain
-rw-r--r--
psyntax.ml4
31128
log
plain
-rw-r--r--
psyntax.mli
948
log
plain
-rw-r--r--
ptactic.ml
8373
log
plain
-rw-r--r--
ptactic.mli
1094
log
plain
-rw-r--r--
ptype.mli
2199
log
plain
-rw-r--r--
ptyping.ml
19465
log
plain
-rw-r--r--
ptyping.mli
1342
log
plain
-rw-r--r--
putil.ml
9011
log
plain
-rw-r--r--
putil.mli
2690
log
plain
-rw-r--r--
pwp.ml
11123
log
plain
-rw-r--r--
pwp.mli
817
log
plain