pristine:ba9ebfd377c04c6a7f03e6e2b81abfae3036fb7acdc893e3adf623cc29d2dbfc
Starting with inventory:
0000520576-d812f71f926a5a5d09ee06d09de6b70818d69c87f48c233fe112afc50d6011f5
[TAG before-breakage
adam.gundry@cis.strath.ac.uk**20110216144445
 Ignore-this: 82e2f899331def19cd59d22bfe361e41
] 
hash: 0000057426-81bd931bb9cb743de58b61afe121cd57e22d2575250d8569b6cbd87ab169cbb0
[Move in the new term representation (breaks the build); here we go...
adam.gundry@cis.strath.ac.uk**20110216145326
 Ignore-this: d58cbdf4edca43a4feac3be7cb8601b7
] 
hash: 0000000745-d335cb19176eef68b6fca4ea31ec5adb87ea6d2e6bebbc99c8fe9d6f5024d2f9
[Merge NameSupply.NameSuppl{y,ier} as Evidences.NameSupply and move Name to Evidences.Tm
adam.gundry@cis.strath.ac.uk**20110216151231
 Ignore-this: 7b4a650f56a49aa7686370dbfcd69a34
] 
hash: 0000013790-51627791226a98fbe894c806e2a1d3e67dbe534b5b9b38e58d9ec4426c383b63
[Fix Epitome (why?)
adam.gundry@cis.strath.ac.uk**20110216151510
 Ignore-this: 1cb5fefd71f9973f22d4d6741b635f85
] 
hash: 0000000378-e1631c9b513d633c347f85cba614f309931ffc56ebfa6402318150ebdfa26848
[deriving instance Can Show
adam.gundry@cis.strath.ac.uk**20110216152753
 Ignore-this: d356296087c31ec28b5f631df88dd7ef
] 
hash: 0000000195-a40516ca95fd6fdd1eec4ac0e74b8727aaa1a987a999e3da7ccae71e29198d2c
[Rename TYPE to TY, (:>:) to (:>>:) and (:<:) to (:<<:)
adam.gundry@cis.strath.ac.uk**20110216153554
 Ignore-this: bc1fac8982e74710ed8b381a2806bbe7
] 
hash: 0000003630-1e612cf4b7f994c462559581994d824f3caa1a0c1e5135863c6f8f3a126f8388
[moreTm
pwm@cs.nott.ac.uk**20110216173947
 Ignore-this: a9662362a9f5e37945685f1f9511bff3
] 
hash: 0000002514-25aa46cbb4c1dbdccae47c9ed1c03b22648775cc00d5d0e6824c204f571e472b
[Update NameSupply and Tm so they work for now
adam.gundry@cis.strath.ac.uk**20110216161514
 Ignore-this: bc29fdab6fbfc036f440c47a62c6d5b6
] 
hash: 0000003406-bd971a378359bc270ed1b8830e58b0f294e0bd2c10191a107f880daa4cc046b0
[DisplayLang stuff
adam.gundry@cis.strath.ac.uk**20110216180135
 Ignore-this: 9dd53971822c99b9b536374c57d1f73
] 
hash: 0000005273-5c4e91695798175b038490fa29ecc1bf237d748b31321af8e36c2c5e41e405e3
[Tm and TmJig magic, plus new canTy
adam.gundry@cis.strath.ac.uk**20110216180213
 Ignore-this: 4a2bee8872865b972ba6b375cb904201
] 
hash: 0000004860-ea09ff8065b17c0a881e6e90b10ab6f9846c46909cc39133cd497a8b58cf4883
[beginnings of etaQuote
pwm@cs.nott.ac.uk**20110216192214
 Ignore-this: fefa6b60ba1037e3972611b0a97b3a8
] 
hash: 0000001140-bc90615930f884c0a528518f51c5878ea12691436491474ece4e4b0220973975
[wrote a bit of typechecker
conor@cis.strath.ac.uk**20110217094934
 
 I've written code which checks canonical terms and lambdas, with the
 raw environment/namesupply management hanging out. This should get
 tucked away neatly later.
 
 I didn't have time to to the change of direction, and we're not ready
 for equality yet, anyway.
] 
hash: 0000002337-79755edaf10be4efe5fffa5f75f0a085e6754eb7e838dc0c35e76e869003c51a
[Move error stuff to a new file
adam.gundry@cis.strath.ac.uk**20110217104047
 Ignore-this: 836d56003803137cc958c33667ba020d
] 
hash: 0000001817-85949c675c0be67d065609ba827b4864cfa1ad9d88652d41e14cc551ea960fa1
[A bit more apply, canTy, chk and ugly
adam.gundry@cis.strath.ac.uk**20110217112348
 Ignore-this: 22b2db832e37fb7f1502f289ad64af93
] 
hash: 0000001649-88abcdea03b25205bb412deb7004a7d644b541ed593898a13eb96d8e7a041f07
[Stk and toBody and suchlike
adam.gundry@cis.strath.ac.uk**20110217130338
 Ignore-this: aaf726cece7b87127b37556bdf6b97db
] 
hash: 0000004153-705a53797259072964a8c3f9bc24793e9296b3b0f0229e7f3106aa92e8cba43c
[Remembered to add EtaQuote.lhs this time
pwm@cs.nott.ac.uk**20110217152344
 Ignore-this: 3b4de25f8b4364f8ed84b2feb059596b
] 
hash: 0000004310-13341761c22de93bd41331850330d5660c8a0793cd085d3bf212d57199dbe9fa
[A little bit of sugar and a Show instance for Tm
adam.gundry@cis.strath.ac.uk**20110218100227
 Ignore-this: b567c9500cd7310f6de4f8fe7fb900a0
] 
hash: 0000000718-faa52eab147ee32ed1fc7d337a93deb0181b250a9ec3aec29dc8194f100e37fa
[Spiny typechecker (needs equality)
adam.gundry@cis.strath.ac.uk**20110218102015
 Ignore-this: ded2de87c776b9a8fe030e4fb376f24a
] 
hash: 0000001505-de63f3b248329c58bae3a90b801c48fc1a3fcf4b3c862f7ef98960a6d3a96983
[some def eq stuff
pwm@cs.nott.ac.uk**20110218104817
 Ignore-this: c5106b472d95c4c67853f4bd1815cd6f
] 
hash: 0000010537-85e938b4feb77725dc448062d2ffa23e2cb935fc911c0f97b7fceddec5faa80c
[Check definitional equality on change of direction
adam.gundry@cis.strath.ac.uk**20110218114403
 Ignore-this: ea247d711dbd36db805ab96e5f42b758
 
 Moves canTy to new file Evidences.TypeCheckRules to break import cycle.
] 
hash: 0000001971-d422a6bfb4e277a004f1e3f3863a76a7b7b482e56b1f7f791aaa8ec4bed6193f
[Brought back Elim functor
pwm@cs.nott.ac.uk**20110218141308
 Ignore-this: 55ab505ed6686d8b63f8c9e288d9b2cf
] 
hash: 0000014794-2f1324168e758f84e8a786b462a4ce46533411b0864da90eb6dbd7838755974e
[Beginnings of a proof state
adam.gundry@cis.strath.ac.uk**20110218163856
 Ignore-this: a5b01b19ad68f76cf9f768534600cc6
] 
hash: 0000014243-ccd8c784a86f0bc06c735a5a2648fc45ce4e7e20b8e96fb3b78ea299d54551b6
[Pushed Elim change to DisplayTm
pwm@cs.nott.ac.uk**20110218171318
 Ignore-this: ecffb37f4e46896866d37269f7a9927f
] 
hash: 0000000553-4be341dae80d4b7e6da2e2340b6ebd91bb00019e1e7a271780964d6c552d6bf0
[Make most of ProofState.Edition compile, if not necessarily correctly
adam.gundry@cis.strath.ac.uk**20110218171115
 Ignore-this: 6680691c68c787caeb90da53123c7e7f
] 
hash: 0000012784-3b4215149cbd4885ff4cd3e507647073c078927bf6d92adae007d45a46dc607d
[Cochon works, albeit with only two tactics: help and quit
adam.gundry@cis.strath.ac.uk**20110218174413
 Ignore-this: 3d4e3fc78de631fb776481bf87ca1b6
] 
hash: 0000007519-4b9e0137856a448b130d2760b82dbdfee6c4142a5f93ddba082c1a4398d8f7c1
[A crummy lam pi sig distiller for ya?
pwm@cs.nott.ac.uk**20110221174024
 Ignore-this: ed01171aad2f87b791945ded85f4d7c7
] 
hash: 0000009022-69bb29db888d9fe47e2b67f6f580837cf30a979c4944ad059adc160d1297fcbd
[Morning warm-up - brought back Prop
pwm@cs.nott.ac.uk**20110222115045
 Ignore-this: ee4123b842859a4999e71a325d241324
] 
hash: 0000011440-6c3706259f3b2ff7d36ae5ba6a1b3fb930de14d9e2dcc5f0da108bb7c3db4377
[Tweak to def eq
pwm@cs.nott.ac.uk**20110222115519
 Ignore-this: ebde87debcb4afcbc8cbc369518ed523
] 
hash: 0000001330-24a4c8dea2e42361bb4d552a694393bebebe46c11a8fb848b5a86b052bc49dac
[My bad
pwm@cs.nott.ac.uk**20110222134021
 Ignore-this: 8be0668947aad7e8515405814c97a22a
] 
hash: 0000002037-6fda6f1783a478d4a2a468d8c44d13baa05423890e2cb2a33421a866a7232bd5
[makeModule
pwm@cs.nott.ac.uk**20110415120227
 Ignore-this: b512a0bd7ee138be0a7062cce6eebf05
] 
hash: 0000014837-0a5389007d5f11b6efd386a8fdddc6bd781bc7f430edfc5b35f7024aa72fba3d
[DumbTrans
pwm@cs.nott.ac.uk**20110418140154
 Ignore-this: f6677548b8a47f40bb5e05a76fc08bea
] 
hash: 0000004203-ca6d2b76d959fa076acd0a7ac3e649d4436d4d44227a7aeb3d98d83822fb6663
[Enable some more Cochon functionality (make, give, lambda, show state)
adam.gundry@cis.strath.ac.uk**20110419130433
 Ignore-this: de020a0550552454f009b38c215b7989
] 
hash: 0000017280-6ba74deeb5ed47ac8785143d5dfbb97e3939452f092640bef196f4cf45fb5725
[Error-reporting chk; equal works at any level (is this right?)
adam.gundry@cis.strath.ac.uk**20110419135757
 Ignore-this: 518d7e5f07ec2f3aac63841b83a74827
] 
hash: 0000005314-261101c9f3cdf145de420469c16f1d80b6e59455a3beaddcc3a57f1961ec191b
[Cope with DEFs in distiller and headTySpine
adam.gundry@cis.strath.ac.uk**20110419145110
 Ignore-this: 881c11a6f5e70f21c5417f9d33295c43
] 
hash: 0000001698-4e49ccec7cfcaf2b0a8ba8599985e6569c11dd66cdf8c5721dc954374fcd182f
[Bring back news propagation, so we don't discard entries when navigating the proof state
adam.gundry@cis.strath.ac.uk**20110420132833
 Ignore-this: b94b9d591f0c598859bded06b4a0cd05
] 
hash: 0000019804-9b0f269556a809342f1f54c1c4ea18168dee873796540eb26b5934b37945c664
[A bit more distill
adam.gundry@cis.strath.ac.uk**20110420134033
 Ignore-this: b6bad275c738e51f8513e1b35317fa2d
] 
hash: 0000001093-1f86ca99d760ff85f6e87d9596c99cc59953d067c58a2e8aa8baba8c24fcf682
[Parameters
pwm@cs.nott.ac.uk**20110421101723
 Ignore-this: 3d7473a43030f7b835cb72cca183449c
] 
hash: 0000002990-92b19fd3ddf5731b2f65c164a3f5d49bf406f4cd193556bb3635d9b831cd7890
[Name resolution, maybe.
pwm@cs.nott.ac.uk**20110421144533
 Ignore-this: 7f7cfedf3b58eea9821ae6ead166ea2d
] 
hash: 0000011082-1d2642aceebe373c810c8235eb542fd4dfdc7d3b3afdbe172438e9d6f752e70b
[Makefile: use hasktags to generate tags, since it is really fast (she is ignored)
adam.gundry@cis.strath.ac.uk**20110421155031
 Ignore-this: 35d4695275e6717a323557335c54d4ff
] 
hash: 0000000293-33950ee4e8e03bd71d8a8515f68aa967da1b72574bb9d56d5d37d1f22b99f6de
[Tm.lhs: renamed eat to eats, added OpMaker, eat, emit, cases, mkDEF, idDEF and switchDEF
james@cs.ioc.ee**20110503163313
 
 Following last weeks discussion in Nottingham with Peter and the email discussion with Conor "[epigram-dev] Implementing DEFs" I added some of the stuff with yet more help from Peter.
] 
hash: 0000002184-412805b8055a1317bb9a13d688d03e63852544beb559daa656f4d1ce23aa09f9
[Added a way to call primative DEFs, added more primative DEFs
pwm@cs.nott.ac.uk**20110506132602
 Ignore-this: 12874adb86dd29fcc0947e1eb035e063
] 
hash: 0000002265-b6262496441558c356db0ca846fa94550c3b60db2465c464cc0a88fd25af6639
[epigram1 web
pwm@cs.nott.ac.uk**20110510095640
 Ignore-this: 32a177d6e236abde9eed73b37760a751
] 
hash: 0000000953-3e48af4b56cd90f9ea8c2447ba7aec0e93d2b6c6b3e157bfad520d1a096b7873
[oops
pwm@cs.nott.ac.uk**20110510100204
 Ignore-this: 6840d1ff78a9e61e685ad6114760b54a
] 
hash: 0000000463-077035e68f4c9d066130192e7165e571f559d69f4955fef96bdad2ab382ba373
[manual
pwm@cs.nott.ac.uk**20110510100813
 Ignore-this: 9634f5efef9fbc6e48478ce7964ad532
] 
hash: 0000000448-b426c5c7521cb1227fac0c89c35cfe6c8e23c2b41eeaa2c45c9f99cb033f3af6
[The little pig is reborn
pwm@cs.nott.ac.uk**20110516144430
 Ignore-this: 670cd8acc2e0d045f16cf3c1198d5c6b
] 
hash: 0000066137-ed0e04a1a12f02eced6c45cfbffe58df12e5b93911de781a6318fd88edf54a81
[an attempt at equality
conor@cis.strath.ac.uk**20110516214210
 
 This is a first attempt at blue equality for Set, Pi, Sigma, Prop, Prf.
 Green equality is no more. I'm sure I haven't got it right yet.
 
] 
hash: 0000010100-97761a02524093a34358598124ef03280cefd19deb24cb723f4f32a1267a445d
[NameResolution? Fixed?
pwm@cs.nott.ac.uk**20110518110049
 Ignore-this: a86f08c109a8a47446a00ce8c30decac
] 
hash: 0000022480-71f5a6986f58e0e9268db31acbf15a2940a45329142d0ad4d0eac078d2d90723
[Enum's back
pwm@cs.nott.ac.uk**20110518151316
 Ignore-this: a3e5af6d5b544aed03f224eec79fa556
] 
hash: 0000013757-d1860358973cef2f2de1f60ef6e116a38351decaf7aad683eb396e0c4fccf3ec
[Make makes again
pwm@cs.nott.ac.uk**20110518151319
 Ignore-this: 6bc7aa1a2e355de6b59eef8c52232a9c
] 
hash: 0000017585-6980bb50d6b8ebb563ad596019b2b30c93d609c1d2830f68b375f29d85806ba4
[Pretty printing Enum
pwm@cs.nott.ac.uk**20110518162145
 Ignore-this: 3623bd7d5c706ef2c62fc3e54782337f
] 
hash: 0000004376-1dd48c6c0bf0a2a59ced0651ed8d62793d8bec0aa9e3ea645513029565e453ed
[Wired Eq to the parser, Elaborator, Pretty Printer
pwm@cs.nott.ac.uk**20110519125827
 Ignore-this: 9a0df680eff542814fe3f922b8880ac7
] 
hash: 0000012426-f435eb73926797bf35db1b17d0b03a00ddc6b63351e13153b2a159080186dbb9
[Quick hack to fix lifting PiParams
pwm@cs.nott.ac.uk**20110519144731
 Ignore-this: 48e89df09b00e4aa290d64125d1eea28
] 
hash: 0000002874-1211fe21fedd54d7af147c278aa33218e41aa4d2b22cd323b6450fb8c6686510
[Fix for the aforementioned hack
pwm@cs.nott.ac.uk**20110519145904
 Ignore-this: 4f62a992b9a46585cc2251424ae8d544
] 
hash: 0000001144-519485e834cfa416d76a34d69b0b467a1f6caa0342d9db6ee8529b00a9a071fe
[Stopped the distiller dropping Eq eliminators
pwm@cs.nott.ac.uk**20110519152733
 Ignore-this: 51fc74e65f7786a10dbdd046647c484e
] 
hash: 0000000644-3c181fa86323510d733d0cc1eb16e300d9d951cff9a568d902b10487d989283b
[isRefl now checks spines for QA _ _ refl
pwm@cs.nott.ac.uk**20110519152800
 Ignore-this: 9486ea08937cbcfb75e54a114f632f22
] 
hash: 0000000423-456650d7314233e433f451194689e154f50aa848e54f09fcb3239299e827f3a1
[Stopped spInf bombing out
pwm@cs.nott.ac.uk**20110519152852
 Ignore-this: c30f2db0d1e457afaab168cd22bc75dd
] 
hash: 0000000315-9d67fb945f2230986ca4d4af168e0dffc0fec948017ae1cd97739262fe45d722
[Various bug fixes
pwm@cs.nott.ac.uk**20110526135806
 Ignore-this: 972da87ab7a33d918c1b1207fe88dc7f
] 
hash: 0000021561-899682ae5e5199c0fa285095c596b01195355f573bc8bd6d8e3a705705bad54c
[inference bug
pwm@cs.nott.ac.uk**20110527122420
 Ignore-this: 4c38b75cb3e574f590bc123090df3f3a
] 
hash: 0000001458-13db8a3139c243e90a48c21941582ae43498768eb407a15e136d706b7e5a559e
[Added name advice to Eat
pwm@cs.nott.ac.uk**20110527123243
 Ignore-this: e5a3ae129d75a8e8c1a7568fbfbb0faa
] 
hash: 0000001851-cc21dea0b0f3f8d1d80569e8afc6de464c66f7536670463dfad80031e5f00af6
[Crummy matching
pwm@cs.nott.ac.uk**20110531101824
 Ignore-this: 36046c331c6120520789e862b2b0037e
] 
hash: 0000007698-669a95b8d9a9b8b6013f3dafb0da52763a78f7197880168a11a2334c6e8725a6
[Bring back schemes (well, partially): use 'let' to create one (but not all the programming problem magic, yet) and 'scheme' to view it
adam.gundry@cis.strath.ac.uk**20110601083204
 Ignore-this: c778c3d477a1b181bf166791d181cdc4
] 
hash: 0000021569-713b89ee72c26d14d4bd507d84eb7a5d4553b1a3d2f962911bc0355e5f5d2c5b
[NameResolution returns Schemes
pwm@cs.nott.ac.uk**20110601084420
 Ignore-this: 8e3afb59a8d88a5d9dc7d75b9d714ed
] 
hash: 0000001397-959bf0530ca44878d814ddaaf993f01f430df52a507f907f79d03b62a0cfec84
[findParam no longer fails badly
pwm@cs.nott.ac.uk**20110601085254
 Ignore-this: bd3271c759cce302f772d40000485c98
] 
hash: 0000000203-ace696438b4f389fe616d40f39960d7fb4bf2d6af7f3ebce667eb9432376ae0e
[Progress on scheme elaboration
adam.gundry@cis.strath.ac.uk**20110601102352
 Ignore-this: 22bb397516c4d0b846b904fd1ce2c505
 
 There are still problems with shared parameters.
] 
hash: 0000007445-423904a0441394611ce88821d9389d43da5f476b8cd69db2b71699ad5d216047
[Handle Suspended tips in news propagation and 'show state'
adam.gundry@cis.strath.ac.uk**20110601104211
 Ignore-this: cbec26533bb4dc9e733bae48a752b0e3
] 
hash: 0000002678-705ea450e7badf87b853f7bdfaecd8c5a1711251e45562458f75d0fd3eeef8e2
[Strip schemes of shared parameters
adam.gundry@cis.strath.ac.uk**20110601114352
 Ignore-this: 73e783e0f5ce7775b0c3a6427f027cea
] 
hash: 0000001209-a9583c9ae1d12516559cd7c7a78ada9936a41e32bd881058e93b673e3e07ffa9
[Env concatenation bug
pwm@cs.nott.ac.uk**20110606132508
 Ignore-this: cbfdfe764cc71e3cc358678b22882fd5
] 
hash: 0000000559-e10de10aa8755bb814493c8aeeb819f24772b1593be1197e7c0944e938e02855
[Ugly-print under closures
adam.gundry@cis.strath.ac.uk**20110606133200
 Ignore-this: 40222235e4a9d8787972adeb24c182d9
] 
hash: 0000001648-be4f4f47a4219945cea6b090dab02113ce91a08de7e5a4242eafd9dd4b4c4e28
[Must train myself to do version control properly
pwm@cs.nott.ac.uk**20110606134013
 Ignore-this: 28019490f2a50cc7cbda42e025d19e3f
] 
hash: 0000021388-68f9d5029c36bb708f348710c96fbdeee45ed64af8d35c95a7d072035ce7aeba
[Parameter tweak
pwm@cs.nott.ac.uk**20110606134401
 Ignore-this: fdeb8d4e38d0158d535e1db23eeff39b
] 
hash: 0000000588-a47238840fbdc41c219e6c0afe5869e380c0f7e61d4bebf51d0a4067a7a2328f
[Oops, forgot to chack the para patch worked :)
pwm@cs.nott.ac.uk**20110606135915
 Ignore-this: 5f82c966bc0493f6b239844f7d6dc3c0
] 
hash: 0000000290-64a61e1f8bb3d8962b49ab4f6487df13817b62097d4c8806f5affae31fd6f5e6
[Fix stupid news propagation typo
adam.gundry@cis.strath.ac.uk**20110606143602
 Ignore-this: fd129b98e144e9c2679e6fdef8079d3b
] 
hash: 0000000331-13748201b75264eca834d7ba4c6b31558e80d35517ea5efe6d2f017efd0038f6
[Added labelling to the 'let' tactic.
pwm@cs.nott.ac.uk**20110608094649
 Ignore-this: 1a73e143e3e47787fdb82b48783c8dd4
] 
hash: 0000010261-8ed24d32c177ba8c47620826facd4b3c50c1c3d2582b0572623cc8f8e2455338
[Don't distill implicits
pwm@cs.nott.ac.uk**20110608101152
 Ignore-this: 3657a2978219a03f6db2ebfa2a987d39
] 
hash: 0000005355-724b2f7a41410a8330a840134b04b5fc620995f44857ab029d0734c3dac7d598
[Fix up the Epitome
adam.gundry@cis.strath.ac.uk**20110610132440
 Ignore-this: ba407848c0f977e229bdd4336d66c4cc
 
 This patch touches a lot of files in order to convert comments so they
 are lhs2TeX friendly. When commenting code, out use < bird tracks
 rather than {- multiline comments -} if you want the Epitome to keep
 working.
] 
hash: 0000064418-53ce20f6a58b4cab45d034badc03200914646431dc6e79ba833f706bf263f658
[New LEnv rep
pwm@cs.nott.ac.uk**20110610144303
 Ignore-this: 3125168ac9dbae007c0eb9e1c41f60ef
] 
hash: 0000011863-09eb130f152e68dda89981cb774a00ace061a52d9c738433256b40e6c9360cc1
[Flipping Schemes fix
pwm@cs.nott.ac.uk**20110610154833
 Ignore-this: a865eae725747e987ebbbc64dd43f086
] 
hash: 0000001288-0aaeec4284567f051a6458bd307e623c7629486b468fd12518068d32222b7599
[Occurs fix wrt new Lenvs
pwm@cs.nott.ac.uk**20110613085414
 Ignore-this: 90a78d09819e4a9f6abc1f467d7f05b9
] 
hash: 0000000932-bc143af32675a40746569c7c5a531fb53a63bc0ace66186313f25d9a399722ce
[ElabLet didn't cope well with global hyps
pwm@cs.nott.ac.uk**20110613111419
 Ignore-this: 7b0c36471e9779fe2956698c78894738
] 
hash: 0000000620-e4f29fe9d2781a2340bbed6678b80a6eb20b854e7213a2574ae185b5477506a7
[EWAM's back (Severely under tested)
pwm@cs.nott.ac.uk**20110613114151
 Ignore-this: 52155492ca478a004713d00ab858e291
] 
hash: 0000026342-309c13dbd93ae7e67a10d0f345187a21fc2da4c94fbfcc0732169906f6645187
[Occurs fix wrt new Lenvs (revisited)
pwm@cs.nott.ac.uk**20110614083920
 Ignore-this: 1b3d72613b50c60f62e26afbb45309c9
] 
hash: 0000001081-907f382d3c20917887c55f703f8aaf15ef0aa727019cef22aa731eee8d6fa3ff
[Some problem simplification
pwm@cs.nott.ac.uk**20110614153900
 Ignore-this: 2e31241849298484bbae46af040f9d74
] 
hash: 0000008574-b7c8dada38c38a1af343e800ce020940906469fc1f32c7f8b8ca269cd4f4ecbd
[subst for Ps when typechecking
pwm@cs.nott.ac.uk**20110628094349
 Ignore-this: b9d268ae91abc64f16fd16169dd1c82d
] 
hash: 0000000275-18bf5a86fd2e3969de673206e13aeb14dd35c21a5d04f481e7b9c22fc3d2cf64
[Data
pwm@cs.nott.ac.uk**20110629145053
 Ignore-this: d9bb32c64d911480bcf5f2291daef68e
] 
hash: 0000022007-59d9b34a80f982455ef78878e4cbceceefbae1941176b184c85081a650ca0c4e
[Induction
pwm@cs.nott.ac.uk**20110630132802
 Ignore-this: 8a323813a5095f36ba7eb638ed3788f
] 
hash: 0000022454-724c92f83baa5a8256daf6b69334d7df0add5af5486fe84983f11b4cb415ba19
[Actually mark on the Stk when case or split happens, rather than just pretend to
pwm@cs.nott.ac.uk**20110704102822
 Ignore-this: 6a037fa198ffb9d73dd648f2205a071
] 
hash: 0000000689-98b23a94710df9daa9c0d826eb2335f2bcf540ed076e9fe9635c86e36b64b069
[Fix eqUnfold bug and shout when unimplemented cases are encountered
adam.gundry@cis.strath.ac.uk**20110705110617
 Ignore-this: 2a20a3345ba4be45903d986e4f5477ef
] 
hash: 0000001230-d0ee455d53cac1467ef469163bde700cadb6d416733926719aaef37552c4c854
[Distill/elaborate out-eliminated proofs, and report errors better in distiller
adam.gundry@cis.strath.ac.uk**20110705110809
 Ignore-this: 7bc17efb7447244509e70fc0ae2e2ada
] 
hash: 0000003517-b91401011cbc7787f9162630affe3f6a9b50728615e3b7eeeecc7fdb033fb84e
[Change |capture| to only require a vector of level numbers, since it was ignoring the type and name advice anyway
adam.gundry@cis.strath.ac.uk**20110705111048
 Ignore-this: fb07fa4209b1e36ccd22ff6ca0a992c9
] 
hash: 0000001154-2de6a982191e177bdee5658b43650e4481ff001f583ba1ebbca36e0e28a7a811
[BVec is Traversable
adam.gundry@cis.strath.ac.uk**20110705111347
 Ignore-this: 2d643688dea624f4ec314fe0066fa8de
] 
hash: 0000000592-a12a2d8692e4475a7358eec9536d6741fc490056d83feba5f43dbde43796c116
[Made D a head
pwm@cs.nott.ac.uk**20110705140917
 Ignore-this: 63d6de415cac7e4463f1ef0271204c9
] 
hash: 0000017665-c059067c0f062954125c1241b4fe3b43d7f30e87c2fca18f9014e2259a3d1c71
[Fixed new workspaces getting the wrong level count when not placed at the tip of parent.
pwm@cs.nott.ac.uk**20110706092124
 Ignore-this: 6f7a0ef8e41a650f439c0a00e2803f26
] 
hash: 0000001068-bcf53525281d7685c57bc9424ec45da210c814f4c95421afa246f32884fa3bcf
[Add case for Out eliminations to the typechecker
adam.gundry@cis.strath.ac.uk**20110707142109
 Ignore-this: d061f86984c47e773f241119502ece0
] 
hash: 0000000960-c4f268c27ad62904bd188f403c10a04f4ce9d4aaff423ddf41cd179db3c31ad9
[Add primitive falseElim to eliminate elements of PRF ZERO (as opposed to just ZERO)
adam.gundry@cis.strath.ac.uk**20110707164226
 Ignore-this: b2a00db9843f215be6ea4418de308a67
] 
hash: 0000000545-bd463d6b5ead867b6f08fc35994024aab28411ccb04f66b59d8804320a64835c
[Add lamLift as a counterpart to piLift in Tm
adam.gundry@cis.strath.ac.uk**20110707164338
 Ignore-this: 3a1129472893ea097e265de8cd39c180
] 
hash: 0000000644-7bc3315e0525360433bb28f3c5114a77cb648f90af0ab36ae9fda259f85f4cb6
[Change behaviour of level environment composition
adam.gundry@cis.strath.ac.uk**20110707164631
 Ignore-this: 8c98203a957edcdd73d86dfa5ca8614d
 
 Since level environments need not be total, we have to take the union when composing them, preferring elements of the inner environment when we have duplicates.
 
 Someone more knowledgeable than me should review this patch.
] 
hash: 0000000671-01b36855c658a720849403368ed1ba0b263dfef2bb2f95acb0a8c044dbf75f7d
[Typechecker: evaluate away more of the irritating redexes
adam.gundry@cis.strath.ac.uk**20110707165139
 Ignore-this: 922cefce78fae17b2bef0f6c0a48cd5b
 
 The idea is that users cannot write redexes, but that we might generate them internally (e.g. in the propositional simplifier), so it should be safe to simply evaluate them. However, this means we need to have a rather large trusted kernel and makes debugging harder. This patch makes the typechecker look for redexes (index variables or applied lambdas) that might be hiding under closures. 
 
 Someone more knowledgeable than me should review this patch.
] 
hash: 0000001229-f2e495a5f374c0e3669c4557d918dd0577c3d6a2d075544249be6853f3daa2e4
[The propositional simplifier lives!
adam.gundry@cis.strath.ac.uk**20110707165752
 Ignore-this: 26c1797f5bc9643c58f9dc53b9b522c0
] 
hash: 0000054982-dd2750eb6df59fc6f875f0408cfcd2ac664dd59dbdf57b5756d154be78231ce5
[Prob simplify now Prop simpifies
pwm@cs.nott.ac.uk**20110714124557
 Ignore-this: 40c823dd608c55dea2526459a3784fc1
] 
hash: 0000006265-95b7de523c981f2f22a95dd5713989d7c1c9c8dd6e303313945dba5aba2c07a0
[substDEF
pwm@cs.nott.ac.uk**20110718140046
 Ignore-this: 3ce0e1c104ea998e61a142d4966c4d3e
] 
hash: 0000000783-7a0146bb47a183577ca6b24d8d64c7c2048c05788b0825de2aefbb4fc2fb5976
[GHC 7 compatibility
adam.gundry@cis.strath.ac.uk**20110718141532
 Ignore-this: 4b8d91ee8e0775a95a3f88d7efad6a08
] 
hash: 0000001756-7701599a7cb6f388f73af4ce100a321be676947622919bfa876460a4b00b4082
[Make ProofState a newtype so we can give a custom fail method in the Monad instance
adam.gundry@cis.strath.ac.uk**20110719092651
 Ignore-this: f27258b90e2cddc21a22e25fe6a49f33
] 
hash: 0000003534-d31f8038f015b024381a48164f0c2fe4b39d25235f081ba23e069275e3286efe
[Fix Parsley to define fail so it doesn't call error
adam.gundry@cis.strath.ac.uk**20110720121546
 Ignore-this: 189ed7d870b8cc3d04c6e3bc1fc858a0
] 
hash: 0000000274-ef90fa2113caa2ab4cc3dcae0b83f6c8f051c3c1275c5fdcb39b459586199fe3
[Massive restructuring of ProofState source files
adam.gundry@cis.strath.ac.uk**20110720105523
 Ignore-this: b834e2e272c3c33212bc8d39db0abe1
] 
hash: 0000075316-4c4de5b4cbf09b44fa32492d668017f3d7aaaa5973a9a5da64660985cf90102c
[Record nix state in developments (name resolution needs fixing)
adam.gundry@cis.strath.ac.uk**20110720122248
 Ignore-this: 1120c7cc5745b419b6b2abbc9dc7ff0
] 
hash: 0000004824-249d503fd46a28a347cf33334b965e02b7ebb7a4656f1c962ac2885b6ad8bea8
[added smart constructor <:/> for :/ and restricted type of :/ to Body-Exp things
conor@cis.strath.ac.uk**20110720140541] 
hash: 0000003122-c8ef9eadd95058a460915c09953abbfc5c61d085e0b18a99f497774470fcb1c2
[apply {Exp} should not run Ds
pwm@cs.nott.ac.uk**20110718150149
 Ignore-this: 93543baed34e2d9fe7040e0dbd33e46a
] 
hash: 0000000203-3628a3e9d07151809b6a9c7db30f8164c432297d4036720a00f9dd36e7680a7c
[applys {Exp} should not run Ds
pwm@cs.nott.ac.uk**20110718150417
 Ignore-this: 2299dc10823551d73e6caec827ae1e45
] 
hash: 0000000214-feca7ce05e73d10bc4625a73f75fd6c84b22289d843f86193e6b86ab27ca7df8
[fixed runOp
pwm@cs.nott.ac.uk**20110718151344
 Ignore-this: e7d20fe177972bc33ca8124e8db36ab9
] 
hash: 0000001642-66a7b86575bd1b725f2f19a2dd3f7f09bdd89132130a0802728dae0d311a65aa
[NameResolution copes with Nix
pwm@cs.nott.ac.uk**20110720143233
 Ignore-this: cc1dfb2846923b86df8136d82195f17d
] 
hash: 0000007625-de345aef46274ea07f41edc457851b1810ae34ce79fce2e82cd01b536408d76b
[New occurs check
pwm@cs.nott.ac.uk**20110720163138
 Ignore-this: e93a832379a128fc1baef0d873d1839d
] 
hash: 0000023106-9fd0d08be5d1e4e39e2f978becc30d971fef26f92c150bf11d80b69fc3ec1be9
[Induction
pwm@cs.nott.ac.uk**20110720171114
 Ignore-this: 14a853f36366a47dde34f9fe04c8c7a2
] 
hash: 0000011351-28c36045a5c7c51107c8a6cd401414b355afbd66e22787a77e8c6c0b2278002b
[Hypothesis nixing: fix Epitome and add HypState to makeModule/makeKinded
adam.gundry@cis.strath.ac.uk**20110720162319
 Ignore-this: a212668289aacea5888fb31af0119b03
] 
hash: 0000006397-2e6799077e39e5419a7e87d90e4a65aaa5df90d029267eb57d19983445463e59
[EWAM works
adam.gundry@cis.strath.ac.uk**20110721161627
 Ignore-this: b110d6065bccb214f3b04b1e6c2ab499
] 
hash: 0000028987-c58f1420b610966feb2c039216ea45d6defcf6b4d99283ad6be913e14d07086a
[evalEager
adam.gundry@cis.strath.ac.uk**20110722093723
 Ignore-this: abdd1c291f96762502df83bbdee99120
] 
hash: 0000000839-f688580dac9012935f989460527113deb84f5c9c28692ced4eeac43a4b9442fe
[Documentation with a motive
adam.gundry@cis.strath.ac.uk**20110722155811
 Ignore-this: e303b5eba01dcf52c71f76ef6bc0fed
 
 The explanation is still poor, and the |elim| function needs some work, but at least there are fewer lies and dead function definitions now.
] 
hash: 0000030993-3b6e602b809fb4f20225cb1da338f23d616e055a60f87d62e85d9dfffa29c63b
[Fix Epitome (change TypeChecker to use lhs2TeX-friendly comments)
adam.gundry@cis.strath.ac.uk**20110722155848
 Ignore-this: 1219d2b4bb17ae99c8fb5de2652e5436
] 
hash: 0000001670-687afcd1769fc2e48c0661fda989ed60b005b564c691e541456218ae97a1f020
[Random tweaks
pwm@cs.nott.ac.uk**20110722092633
 Ignore-this: 865753ccd6fc576296fe96b6c48936fd
] 
hash: 0000000686-6f809ce8c8aa002e30aa49fe014402697c3eecab2e038104e5eee2f6e8140b33
[evalEager a bit more
pwm@cs.nott.ac.uk**20110722104410
 Ignore-this: 5aa223bbc097b7521914b7072bcf2b18
] 
hash: 0000002898-5a22e519d47afa4cc2fc6a7ded7c9047b4c95ffa5ff5067ee589ff393a8d9f76
[BUG fix: Name resolution from inside Nix'd modules.
pwm@cs.nott.ac.uk**20110725123955
 Ignore-this: bd046c86f9e5b2d8ffd66b8cfe749b40
] 
hash: 0000004590-53f9337ace9dfc709af1dea33abc8262cda64ddbd0a64e6f8bd03f7ca2b6e641
[fortran now uses name advice from Eat
pwm@cs.nott.ac.uk**20110725124656
 Ignore-this: c93812006163d5d6329f1d38b7693993
] 
hash: 0000000365-6181db9a1d9415561345953c4db7194672b559570e8763a04b6bf18cc508cac2
[Distill tagged data types nicely
pwm@cs.nott.ac.uk**20110726090605
 Ignore-this: 86ffa36d029c5edf6cc08a716325963c
] 
hash: 0000000985-0744cf19dd8993487a939bf0479ceffaeb1bdd12498a161c148962e3ee73a58d
[Fixed etaQuote for prfs
pwm@cs.nott.ac.uk**20110727125958
 Ignore-this: da37e696855d4f57a86044d29fca9aba
] 
hash: 0000004688-b0078973b1f9c8c769f2778d6ef51361a5afff4acdaf9aea82a45aa26ca29dfc
[Slightly hacky attempt to get nice names when using Desc
pwm@cs.nott.ac.uk**20110727154528
 Ignore-this: 1edc469ce34732985f7c6299fb7fc408
] 
hash: 0000001825-aeb99f61262e14648dd7df21b157bf0032442066bd23e5f88076c9d984c89aa9
[seekLabel is now Level safe
pwm@cs.nott.ac.uk**20110728102314
 Ignore-this: 8671d00a86231e7092d67c01b7857078
] 
hash: 0000000855-31e47103b36604ee7f107b3653df44b4879b8465783e429491648d34a9fbc458
[2 + 2 is 4 (2011 version)
pwm@cs.nott.ac.uk**20110728133423
 Ignore-this: 56eb860f94d944cd01938dd458035064
] 
hash: 0000001505-5e4fd86ef0b80404ecfeaf7d24d7fcc52097617f836f5f80e67b4198422d4555
[added agda model of list-style datatypes
conor@cis.strath.ac.uk**20110729121359] 
hash: 0000008525-ae441f66dd05042e36df6f40640c156bee726d9a2dd68eb5097369410cec4c42
[Can define Fin now
pwm@cs.nott.ac.uk**20110729144547
 Ignore-this: 89451a286891c14e6ed90fb6b9fe5aee
] 
hash: 0000001002-6386f7b1bd8b42c910ad3e3e458b297ccc5d09b6ae4f76eaa4953455fc423979
[commented out the instances she now builds
conor@cis.strath.ac.uk**20110802114118] 
hash: 0000005392-5a1c5c0b41fb7b627e123eece84e5c5c18ea0c0aff4acd194cd90002aafe172e
[Alternative from MonadPlus in Parsley
conor@cis.strath.ac.uk**20110802120420] 
hash: 0000000523-8ada6b7953eb30e9728b017be32099f04b278c29729e4f9d9279e25f976f5833
[infixr <>>, sketched a source lexer
conor@cis.strath.ac.uk**20110802212314] 
hash: 0000004874-f98f39a32cd0278f9442f2930815847cf138ff297f6d1df4160a505b0c9b9bb2
[bar tweaking in lexer
conor@cis.strath.ac.uk**20110803112318] 
hash: 0000000885-9f33fdb9b3c3f54d8ed7dd18c59d7600319800f620f607d96b178604937ebd0c
[Deal with pars of data-types correctly
pwm@cs.nott.ac.uk**20110802103809
 Ignore-this: 3e5916e0a7e549045e0e2a00e58241f9
] 
hash: 0000000863-e4aa636568d0b5dd14ab32126c8e90bdeebc71e852c506e2ab4973cf7dd74f68
[Fixed the distiller for ghc7 compilation
pwm@cs.nott.ac.uk**20110804094709
 Ignore-this: 139a6af0f9c44473feec0ddd10d2f4ba
] 
hash: 0000000773-940b300bfa5b404e339eb7ee8aa8a366f8123706c33b2982a091149017572b1f
[Levitated Enum
pwm@cs.nott.ac.uk**20110804122542
 Ignore-this: 456f1d05d50e91ead2b842e0e43539a9
] 
hash: 0000007954-9b2faaf91a0ec9fc2d18e68d92889a4edcc2d2be13a6bba03a13a0419e41fbc6
[Temporarily hard coding lists for data type fun (later)
pwm@cs.nott.ac.uk**20110804132527
 Ignore-this: 7341a3b0e8e062adb94cc7089db70ad
] 
hash: 0000003211-b4d518c2eeb8ac94a9a1bd412d3abd4c649a6e0d071a4a815e9ce171d4861c11
[Blue head terms, proof of concept
pwm@cs.nott.ac.uk**20111026094159
 Ignore-this: 567e18d6c9df383670f502ba694600c3
] 
hash: 0000015209-7a206a08e6f0a093727aa8c6a58e507e45a44b9e9007227da4263db56c6a5788
[another crack at a datatype for the source language
conor@cis.strath.ac.uk**20111103124437
 
 I've forgotten what I did to the lexer.
 
 I've added a directory called "wishing" with mockup source files.
 I've added a file SourceLang/SourceData with datatypes for the syntax
 of the source language. Every node has a source annotation (currently
 dumb). Some SHE-nanigans are deployed to keep problems and strategies
 compatible with definition kinds (data, let, lemma).
 
] 
hash: 0000008829-3dc0a0540d9d0352df1c47978287ab97fc421dc958090ef9793ab3788b1b7603
[Switched to the eager eval to avoid space leak (temp fix!)
pwm@cs.nott.ac.uk**20111103153458
 Ignore-this: a119b8819eaf3a9ef24c656636214dfe
] 
hash: 0000000346-647a25b18dd464d86865bb314cec621f548ae9aff3a5a5f8fc2562f4ab902e62
[1st class schemes
pwm@cs.nott.ac.uk**20111103153534
 Ignore-this: 5c9dd6011c772f5dfa73760e97e5ed93
] 
hash: 0000002588-432fe92d0c2b0a36c7a5e254fe24a524b52583065129ad7d888de3cd33911249
[Dub types
pwm@cs.nott.ac.uk**20111103161215
 Ignore-this: 4d2b480d7c980b11086f8decbfb073c7
] 
hash: 0000000962-a5ccaf82bd3b0e6321578f45557c63eff3e25d43091a1b17847c4d4cde7bf2a0
[Problems as types
pwm@cs.nott.ac.uk**20111103173344
 Ignore-this: ee5f1782274157d3b2459d451c169d67
] 
hash: 0000001615-2dc1ffb3b6ca5b364e9816ef754efd91f26cdfce07256db9882a6800dff5c168
[Split Equality into Set and Value variants
pwm@cs.nott.ac.uk**20111104120759
 Ignore-this: aff7fbd78cf55c50f2adc7ccdc2f9505
] 
hash: 0000013932-99aa9c6c52320097074101632bafab17e140dd1de8e190c21497817929190af2
[Hoping for proofs triggers prop simp now
pwm@cs.nott.ac.uk**20111115154242
 Ignore-this: 49bbe4835fb0d86157d2dc26f3426a26
] 
hash: 0000002682-4a2574968991da1d9533b2caa939b4b5b0c5017caf60ff3515a16efaa207aed9
[New elaborator started
pwm@cs.nott.ac.uk**20111124110909
 Ignore-this: d0c7f066f15486233ee4ec481f12c159
] 
hash: 0000020201-f7ef0611a08e7599cfc66ee24318fe21a821355832e2cc41250e4ebf0db95091
[Fixed Epitome
pwm@cs.nott.ac.uk**20111124161902
 Ignore-this: f0ded356df77d3becef5780eb934c263
] 
hash: 0000000493-80aad02d643e9d2ce70cca39bf329b42fed3e1c230d404160f0013cd302ed0c3
[grammaria
conor@cis.strath.ac.uk**20111124153355
 I've added a treatment of layout to the Lexer, so a document
 is now a [Nest], where data Nest = [Elt] :# [Nest], so that's a header
 line and a subordinate document.
 
 There's a new parser library, Parx, which lets you grab the token extent
 that a parse consumed. I've tweaked SourceData to reflect those token extents.
 
 Note that some constructs are "vertical" and parsed over Nest "tokens", while
 others are "horizontal" and parsed over Elt tokens.
 
 I forgot to add the file for the beginning of the parser.
] 
hash: 0000014300-1c8b35f19b03c90f10617925e1d6bcb2fb04e737fa4be43282e02266aaa40adb
[parser kickoff
conor@cis.strath.ac.uk**20111124154018
 
 SourceParser is the parser for Epigram source. Not very much of it is
 written yet, but we should be able to parse simple signatures.
 
 Much more to come...
 
] 
hash: 0000005556-2121ed5936061b1886a7ac89bcdfe5304c92307bb20871f395fa14dddd6cfde0
[merge-o-matic
conor@cis.strath.ac.uk**20111124162301] 
hash: 0000000474-28998be2ab3686996d444874e03307a95c64ff9db77f696983f204fa3a3661de
[; is white, 2d style has more padding
conor@cis.strath.ac.uk**20111124164032] 
hash: 0000001480-172893e5d048ac53182e09603602b9a8cda35d3d45a9632aed7911a456fc62aa
[simplified rules about semicolons and added braces
conor@cis.strath.ac.uk**20111124173423
 
 I realised that I was getting ; a bit wrong, so I've fixed things.
 A semicolon is always a top-level newline in the current layout stack.
 To localize the layout stack, use braces.
 
 So
 
   let f : Set; ...
 
 is *bad*, because the let has no dialogue and the ... is in the place of
 a new definition.
 
 But
 
   let {f : Set; ...}
 
 is *good*, because the ... is now in the right place to stand for the
 missing dialogue.
 
 You can also avoid semicolons by writing the *good*
 
   let f : Set
     ...
 
 but the indentation is important. But
 
   let f : Set
   ...
 
 is *bad*, because again, the ... is not subordinate to the let.
] 
hash: 0000002671-a886e9ef592ff3b7f89caf7bcc0b94fe3a4630bee002bbd3315da1bfec376971
[quite a lot more parsing
conor@cis.strath.ac.uk**20111124204948] 
hash: 0000006098-5fe1131af6889f53e8494ee07e1f041e417c9bdf7f2756e63423fc23812bfe17
[added padding
conor@cis.strath.ac.uk**20111126143238
 
 The lexer leaves whitespace intact, so we have to remember to allow for it.
 Moreover, the grouper puts in extra layout information, with a view to
 supporting the exact reconstruction of the original text.
] 
hash: 0000000833-1f360f02bc961f28534228951097ad5e1224652a25d8db427b1b90b51b8963fd
[Ambulando is reborn -- breaks most cochon commands
pwm@cs.nott.ac.uk**20111213181455
 Ignore-this: 49294e98c1cd5590c8bde69fa6efb4d5
] 
hash: 0000057295-c1c71dc449a18740b24aece15ad3fb3b13c9f723e7f9d026e2994c6e7fcd717e
[Oops, here he is
pwm@cs.nott.ac.uk**20111213182121
 Ignore-this: 26f6b96336b770183f2e2999ecd7aa96
] 
hash: 0000013310-611373cb8f5b05bb8bb7cc7e2f165e25b4321b5099ad0870d83e2225324df38f
[Bug ficing elaboration
pwm@cs.nott.ac.uk**20111214184254
 Ignore-this: 74b6bd980369069afaf3fe824c6a1156
] 
hash: 0000014661-6fbe2848f40264b22fa01f4961c9dbec2f297244808fd1676e89e8935aa81a0d
[elab Pi
pwm@cs.nott.ac.uk**20111215120611
 Ignore-this: 25b3aecad5ea60080d0cc50b43d85d07
] 
hash: 0000003382-6db38ac9bb2731b423b89f25d9bf07591e5787e9af08027ef3034e82c4014a72
[Unfinished monkey business
pwm@cs.nott.ac.uk**20111215193243
 Ignore-this: db0657ad0cb75d127bd6473501cad450
] 
hash: 0000012520-a152dccae6da2ff1a98d6ae4fe00fab3391815bb7e452bf33331ef95c980e588
[Conchon meet Parx, Parx - Cochon
pwm@cs.nott.ac.uk**20120106140350
 Ignore-this: eb09e58c010689b2ef96473abbbcb418
] 
hash: 0000024640-8e9068074ba20337ad25cc7905e6bd906bcb0a691fba8e63ba65810d02db89d2
[Whoops
pwm@cs.nott.ac.uk**20120106141349
 Ignore-this: 2915d7a76b9e6b8b56f9f55590ce004b
] 
hash: 0000000275-59c6d71c51713ad984983504c418e9cd9b0d0ccbe3e4d93438b0b681fe038302
[Hoping for a proof of a reflexive eq gives refl
pwm@cs.nott.ac.uk**20120106142747
 Ignore-this: 7aaa7f3cb1edb1bf7be4d1289cc7890f
] 
hash: 0000000664-231a2959f429ce821ad753cafe0804f8f3560761a5894ede4bc033dc55ef3e99
[exTm elab in Cochon
pwm@cs.nott.ac.uk**20120106150515
 Ignore-this: 96a7c96644673366229f6c50f654c290
] 
hash: 0000001190-49a9faf47da23ad1f9d68f9e83d404e829062237930f7159daf6f7b0cc139c30
[Mare graceful failure when mispalling tactic names
pwm@cs.nott.ac.uk**20120106152023
 Ignore-this: f720e84ee1dac40b643859a9774fc254
] 
hash: 0000000529-4f76a0fd3152f90b1bb3cbadedceb1312aafd88b7ee340d6004f93c86f31bdb6
[Better fix - now deals with ambiguity
pwm@cs.nott.ac.uk**20120106154308
 Ignore-this: 6ed9aa112a5cbc039bffa2797e8f8c4f
] 
hash: 0000000658-1f2ba7fdc13d8eeee3ddf0ca29d7811738aad0d8ec78d55d53210aacc57fec72
[More unification in elaboration
pwm@cs.nott.ac.uk**20120113161149
 Ignore-this: 9a80fa5c193f1c960b028115be73262d
] 
hash: 0000014513-63a33921a297ca674c302669fc3f28e1f9f194dcaeae7541a196e290f23d5992
[We need higher-order unification, but we aint got it
adam.gundry@strath.ac.uk**20120216170627
 Ignore-this: 3fe519724a44aacfe69b192271ba58b6
] 
hash: 0000003521-36acdc187400be234280304d3613bb0dc250393b4bc4c8ecb18edad49e93298e
[compiling under 7.4; no idea what it does
conor@cis.strath.ac.uk**20120509101057] 
hash: 0000005154-18b6fefaeff6fd7cd09b13a9f9d0e82b7a3052f6196bd29da87d65bd9eac939e