[Initial import Matthieu Sozeau **20070130115031] [Use digits instead of lists Matthieu Sozeau **20070201102222] [Try notation Matthieu Sozeau **20070203211542] [Work on finger trees Matthieu Sozeau **20070204192109] [Work on finger tree Matthieu Sozeau **20070204205458] [Build the Measured implementation Matthieu Sozeau **20070205172521] [Work on split Matthieu Sozeau **20070206021415] [Work on split proof, hard Matthieu Sozeau **20070206201243] [Move tactics out of the way Matthieu Sozeau **20070207153411] [Build the dependent measured implementation Matthieu Sozeau **20070207183445] [Advance work on dependent finger trees Matthieu Sozeau **20070208002953] [Catenation with dependent version done Matthieu Sozeau **20070208024158] [splitDigit done, badly Matthieu Sozeau **20070208112501] [Work around the splits... Matthieu Sozeau **20070208174151] [Forgot to add Split for digits... Matthieu Sozeau **20070208174236] [Finished a first depend implementation, only missing a property on split Matthieu Sozeau **20070208230447] [Begin coding examples Matthieu Sozeau **20070209015618] [Work on ord seq Matthieu Sozeau **20070209112323] [Fully dependent version done, only problem is isEmpty Matthieu Sozeau **20070209170829] [Forgot to add Split for digits... Matthieu Sozeau **20070209184621] [Proper dependent split definition, now relying only on JMeq_eq for the isEmpty case (ie: pretty safe) Matthieu Sozeau **20070209203642] [Stronger split spec, work on ordseq Matthieu Sozeau **20070209231002] [View_L has a measure, hence we can define functions by rec on it Matthieu Sozeau **20070210133622] [Separated Digit implementation Matthieu Sozeau **20070210133640] [List Monoid implementation Matthieu Sozeau **20070210133655] [Fix split Matthieu Sozeau **20070210140051] [Change destructuring let notation Matthieu Sozeau **20070210162916] [Documentation and clean-up Matthieu Sozeau **20070210173820] [Work on article Matthieu Sozeau **20070210195149] [Begin article Matthieu Sozeau **20070210230326] [Clean things, continue with article Matthieu Sozeau **20070211015233] [Add monoid example Matthieu Sozeau **20070211015930] [Comments on DependentFingerTree for jfp Matthieu Sozeau **20070211042953] [Work on presentation of the type system Matthieu Sozeau **20070211133937] [Clean up organization of code, work on paper Matthieu Sozeau **20070211173252] [Use implicit arguments where possible Matthieu Sozeau **20070211175615] [Missing files Matthieu Sozeau **20070212111007] [More hiding, cons_L to consL for less typing annotations Matthieu Sozeau **20070212190238] [Continue documentation of finger trees Matthieu Sozeau **20070212214441] [Work while talking to Claire Matthieu Sozeau **20070213004416] [Reread Matthieu Sozeau **20070213015427] [A bit of work Matthieu Sozeau **20070214164515] [Adapt to new syntax and stuff :) Matthieu Sozeau **20070216173628] [Fixes from the train Matthieu Sozeau **20070216211706] [Li'll fix Matthieu Sozeau **20070216213216] [Move non-dep itf away, update the first instances Matthieu Sozeau **20070217194249] [Developed dependent sequence, with dependent spec, and defined certified get and set impls Matthieu Sozeau **20070218181206] [Finish get/set, cleanup code Matthieu Sozeau **20070218234221] [Files for making the extracted code Matthieu Sozeau **20070219002042] [Forgot extract file Matthieu Sozeau **20070219165207] [Proper get/set proof Matthieu Sozeau **20070219155250] [Christine's magic incantation Matthieu Sozeau **20070219170231] [Set up extraction for HS and continue paper Matthieu Sozeau **20070219175503] [Work on dependent sequences Matthieu Sozeau **20070220180617] [Finish splitAt proof Matthieu Sozeau **20070223170559] [FingerTree pb Matthieu Sozeau **20070228110643] [New abbrevs, work on dep seq Matthieu Sozeau **20070308140630] [Work on size of trees Matthieu Sozeau **20070311094601] [Update to new publi and add set_get_diff lemma Matthieu Sozeau **20070313215230] [Beginning of fixes from Yannick Matthieu Sozeau **20070313220020] [Fixes from Yannick Matthieu Sozeau **20070313232013] [Work on fonts, adapt to sigplan style Matthieu Sozeau **20070314171139] [More consisten naming convention, make things compile again Matthieu Sozeau **20070314204328] [Make it compile again Matthieu Sozeau **20070320005757] [Make everything work again :), except Dependent Sequences unfinished Matthieu Sozeau **20070321175311] [Work on paper Matthieu Sozeau **20070322000142] [Work on intro of paper Matthieu Sozeau **20070322134607] [Work on paper, introducing sections Matthieu Sozeau **20070322161615] [Work on paper, intro to Russell needs examples Matthieu Sozeau **20070322172715] [Work on biblio, small fixes in intro Matthieu Sozeau **20070322211633] [Work on paper, christine fixes, some beautifying, some more explanations Matthieu Sozeau **20070323175916] [Add example fingertree Matthieu Sozeau **20070324112109] [Fixes from the train Matthieu Sozeau **20070324212334] [Add paragraph on pattern matching, redo figure using tikz Matthieu Sozeau **20070325155541] [Minor fixes Matthieu Sozeau **20070325161454] [Update to latest Program version Matthieu Sozeau **20070326161446] [Work on sequences Matthieu Sozeau **20070327122151] [Work on end of paper Matthieu Sozeau **20070328083148] [Work on dependend sequences Matthieu Sozeau **20070329115137] [Work on dep seq, at split Matthieu Sozeau **20070329164913] [Better proofs and code in DependentSequence Matthieu Sozeau **20070329195133] [Finish first draft or paper Matthieu Sozeau **20070329215843] [Minor typo Matthieu Sozeau **20070330190442] [Fixes from JCF Matthieu Sozeau **20070330230640] [Adapt to new macros Matthieu Sozeau **20070402145056] [Fixes from Christine: a beginning Matthieu Sozeau **20070402181102] [Work on figure Matthieu Sozeau **20070402214708] [Afternoon work on views, reduce code size... Matthieu Sozeau **20070403143517] [Compile againg Matthieu Sozeau **20070403151222] [Work on end Matthieu Sozeau **20070403181811] [Minor fixes at rereading Matthieu Sozeau **20070403193920] [Fixes on the end by Christine Matthieu Sozeau **20070404171318] [Fixes from Adam, Christine Matthieu Sozeau **20070404233955] [Fixes from christine and general rereading Matthieu Sozeau **20070405162026] [Finalized version Matthieu Sozeau **20070405212444] [Minor fixes, have to check biblio and typesetting Matthieu Sozeau **20070406081155] [Type fixes, a4paper Matthieu Sozeau **20070406115134] [Pre-submission fixes Matthieu Sozeau **20070406155803] [Reorganize Matthieu Sozeau **20070406162322] [Pull files from other repos Matthieu Sozeau **20070406164650] [Extraction working in new organization Matthieu Sozeau **20070406165520] [Work on archive of fingertrees Matthieu Sozeau **20070406174504] [Adapt README Matthieu Sozeau **20070406180303] [Minor tactic change Matthieu Sozeau **20070505101350] [Author response Matthieu Sozeau **20070524130910] [Full response Matthieu Sozeau **20070525153501] [Work on response Matthieu Sozeau **20070525155045] [Submitted paper to ICFP'07 Matthieu Sozeau **20070613123655] [Little work on Digit Matthieu Sozeau **20070613144815] [Back to split dev. tree Matthieu Sozeau **20070613145122] [Work on reviewers comments Matthieu Sozeau **20070613145156] [Makes everything compile again with trunk, work on corrections Matthieu Sozeau **20070614110657] [Finish making corrections from referees Matthieu Sozeau **20070614164042] [Minor fixes due to bib and style changes Matthieu Sozeau **20070618140956] [Finish corrections Matthieu Sozeau **20070620150849] [Replace sheard citation Matthieu Sozeau **20070620151751] [Add makebib.sh and replace.mll Matthieu Sozeau **20070620151849] [Fixes in the header of the paper Matthieu Sozeau **20070620154429] [Categories and subj desc, rework abstract Matthieu Sozeau **20070702111928] [Last typo fixes before subm Matthieu Sozeau **20070702114558] [Script to build submission files, clean makedoc script Matthieu Sozeau **20070702122330] [Last fixes from christine Matthieu Sozeau **20070710133055] [Fix from normam Matthieu Sozeau **20070712194014] [Last fixes before sending Matthieu Sozeau **20070719174757] [Fix to get back to 12 pages Matthieu Sozeau **20070719180414] [Submitted final version Matthieu Sozeau **20070719205010] [Begin slides for ICFP Matthieu Sozeau **20070916230723] [Prepare begining, fix style Matthieu Sozeau **20070917162620] [Work on slides Matthieu Sozeau **20070918144443] [Update for coq trunk Matthieu Sozeau **20070925124453] [Work on slides Matthieu Sozeau **20070925124530] [New version using modules for efficient ocaml extraction, setup a string module to allow pluging into the ICFP code Matthieu Sozeau **20070925165325] [Work on impl for ICFP Matthieu Sozeau **20070925222842] [Full implementation of ropes with efficient ops Matthieu Sozeau **20070925223914] [Better slides, more abstract and targeted at the right audienc Matthieu Sozeau **20070926103541] [Fix bugs in get Matthieu Sozeau **20070927144203] [Work on better slides Matthieu Sozeau **20070928134156] [Better rope impl, only 3 to 4 times slower than JCF Matthieu Sozeau **20070928134227] [Last min fixes Matthieu Sozeau **20070928160807] [Fixes from CP Matthieu Sozeau **20070928195348] [Last fixes Matthieu Sozeau **20071008174451] [Move theme to publications repo Matthieu Sozeau **20071008174546] [Add used slides Matthieu Sozeau **20071008174649] [Update to latest coq version, prepare for a quick release Matthieu Sozeau **20071025132040] [Add files for release Matthieu Sozeau **20071025132110] [Workaround bug in extraction, correct dependencies for extracted ML code Matthieu Sozeau **20071025133827] [Extraction without lists and reduce, put makedoc script Matthieu Sozeau **20071025135211] [Put globals.dump so as not to have to rebuild them to do the documentation Matthieu Sozeau **20071025135819] [Forgot some files for Ropes Matthieu Sozeau **20071025135914] [Port to monoid typeclass Matthieu Sozeau **20080924085104] [Rollback port to monoids. Matthieu Sozeau **20080924085841] [Port to latest coq and program Matthieu Sozeau **20080924151933] [Finish port to new Numbers Matthieu Sozeau **20080924210742] [Finish resolving typesetting issues Matthieu Sozeau **20080925073935] [French comments Matthieu Sozeau **20080928205950] [Finish translation to french Matthieu Sozeau **20080930130350] [Up to half of DependentSequence translated Matthieu Sozeau **20080930160753] [Finish dependent sequence translation Matthieu Sozeau **20081001164208] [Minor fixes Matthieu Sozeau **20081002130252] [Minor fixes Matthieu Sozeau **20081002150950] [Various fixes Matthieu Sozeau **20081012155947] [Port to typeclasses Matthieu Sozeau **20081012183831] [Typesetting issues Matthieu Sozeau **20081012194023] [monoid -> Monoid Matthieu Sozeau **20081012202754] [Retypeseting given coqdoc Matthieu Sozeau **20081014210321] [Typesetting issues in Finger Trees Matthieu Sozeau **20081016132456] [Fixes on FTs by Pottier Matthieu Sozeau **20081206130904] [Instance Global fix Matthieu Sozeau **20081206160952] [Port to coq trunk Matthieu Sozeau **20090223142821]