coq-hetmet.git
13 years agobetter names for the auxiliary CaseBranch records
Adam Megacz [Mon, 7 Mar 2011 13:41:43 +0000 (05:41 -0800)]
better names for the auxiliary CaseBranch records

13 years agoseparate type/coer/expr variables in HaskWeak case branches
Adam Megacz [Mon, 7 Mar 2011 13:41:40 +0000 (05:41 -0800)]
separate type/coer/expr variables in HaskWeak case branches

13 years agostore variables in ELetRecBindings rather than its indexing tree
Adam Megacz [Mon, 7 Mar 2011 13:41:37 +0000 (05:41 -0800)]
store variables in ELetRecBindings rather than its indexing tree

13 years agoadd HaskWeakToCore
Adam Megacz [Mon, 7 Mar 2011 13:41:35 +0000 (05:41 -0800)]
add HaskWeakToCore

13 years agoadd proper proofs of the fact that every rule has exactly one conclusion
Adam Megacz [Mon, 7 Mar 2011 13:41:33 +0000 (05:41 -0800)]
add proper proofs of the fact that every rule has exactly one conclusion

13 years agoChanged WEBrak/WEEsc to store a CoreType
Adam Megacz [Mon, 7 Mar 2011 13:41:30 +0000 (05:41 -0800)]
Changed WEBrak/WEEsc to store a CoreType

13 years agoAdded WeakVar, a separate variable representation for HaskWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:27 +0000 (05:41 -0800)]
Added WeakVar, a separate variable representation for HaskWeak

13 years agoadded "publish" target to regenerate tex/pdf code
Adam Megacz [Mon, 7 Mar 2011 13:41:24 +0000 (05:41 -0800)]
added "publish" target to regenerate tex/pdf code

13 years agoadded HaskCoreToWeak
Adam Megacz [Mon, 7 Mar 2011 13:41:17 +0000 (05:41 -0800)]
added HaskCoreToWeak

13 years agocleaned up lots of FIXMEs in ProofToLatex
Adam Megacz [Mon, 7 Mar 2011 13:40:58 +0000 (05:40 -0800)]
cleaned up lots of FIXMEs in ProofToLatex

13 years agoInitial checkin of Coq-in-GHC code
Adam Megacz [Wed, 2 Mar 2011 22:25:04 +0000 (14:25 -0800)]
Initial checkin of Coq-in-GHC code