projects / coq-hetmet.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 693c6f5) | patch
add EGlobal/RGlobal for CoreVars whose binder we cannot see
authorAdam Megacz <megacz@cs.berkeley.edu>
Wed, 16 Mar 2011 08:52:39 +0000 (01:52 -0700)
committerAdam Megacz <megacz@cs.berkeley.edu>
Wed, 16 Mar 2011 08:52:39 +0000 (01:52 -0700)
commitff9fafbf161b4f12688d5986518be874d39ab3ee
tree820634bd37bba1a5f69af3d9e305f9a869e4fc7dtree | snapshot
parent693c6f552555f14c085a71e0b03c67d3c051eaa1commit | diff
add EGlobal/RGlobal for CoreVars whose binder we cannot see
src/HaskProof.v diff | blob | history
src/HaskProofToLatex.v diff | blob | history
src/HaskStrong.v diff | blob | history
src/HaskStrongToProof.v diff | blob | history
Coq proofs and code accompanying the HetMet extensions for GHC