projects / coq-hetmet.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(initial) | patch
Initial checkin of Coq-in-GHC code
authorAdam Megacz <megacz@cs.berkeley.edu>
Wed, 2 Mar 2011 22:25:04 +0000 (14:25 -0800)
committerAdam Megacz <megacz@cs.berkeley.edu>
Wed, 2 Mar 2011 22:25:04 +0000 (14:25 -0800)
commit112daf37524662d6d2267d3f7e50ff3522683b8f
treeaf5ad1ab40a8dbfe1b42f46d12412ea41b6519a0tree | snapshot
Initial checkin of Coq-in-GHC code
18 files changed:
.gitignore [new file with mode: 0644] blob
Makefile [new file with mode: 0644] blob
src/Extraction-prefix.hs [new file with mode: 0644] blob
src/Extraction.v [new file with mode: 0644] blob
src/General.v [new file with mode: 0644] blob
src/HaskCore.v [new file with mode: 0644] blob
src/HaskCoreTypes.v [new file with mode: 0644] blob
src/HaskCoreVars.v [new file with mode: 0644] blob
src/HaskGeneral.v [new file with mode: 0644] blob
src/HaskLiterals.v [new file with mode: 0644] blob
src/HaskProof.v [new file with mode: 0644] blob
src/HaskStrong.v [new file with mode: 0644] blob
src/HaskStrongTypes.v [new file with mode: 0644] blob
src/HaskWeak.v [new file with mode: 0644] blob
src/Main.v [new file with mode: 0644] blob
src/NaturalDeduction.v [new file with mode: 0644] blob
src/NaturalDeductionToLatex.v [new file with mode: 0644] blob
src/Preamble.v [new file with mode: 0644] blob
Coq proofs and code accompanying the HetMet extensions for GHC