]> matita.cs.unibo.it Git - helm.git/history - matita/matita/lib
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
syntactic components detached from basic_2 become static_2
[helm.git] / matita / matita / lib /
2018-04-20 Ferruccio Guididecentralizing core notation continues ... tree | commitdiff
2018-03-29 Ferruccio Guididecentralizing core notation tree | commitdiff
2016-11-24 Ferruccio Guidilexer updated with the new reference syntax + tree | commitdiff
2016-04-18 Ferruccio GuidiAs required by M. Maietti, tree | commitdiff
2016-03-13 Ferruccio Guidi- new syntax for let rec/corec with flavor specifier... tree | commitdiff
2015-01-07 Claudio Sacerdoti... ... tree | commitdiff
2014-12-24 Andrea Aspertiremoving some old files tree | commitdiff
2014-12-24 Andrea Aspertifinite lambda calculus tree | commitdiff
2014-12-23 Andrea AspertiA compiling version tree | commitdiff
2014-12-23 Claudio Sacerdoti... check removed tree | commitdiff
2014-12-04 Andrea Aspertifixing tree | commitdiff
2014-12-04 Andrea Aspertifixing tree | commitdiff
2014-12-04 Andrea Aspertifixing tree | commitdiff
2014-10-21 Claudio Sacerdoti... Typos. tree | commitdiff
2014-09-17 Andrea Aspertibig_O.ma tree | commitdiff
2014-09-17 Andrea Aspertitoolkit.ma tree | commitdiff
2014-09-11 Claudio Sacerdoti... ... tree | commitdiff
2014-09-11 Claudio Sacerdoti... ... tree | commitdiff
2014-09-10 Claudio Sacerdoti... New chapter on setoids. tree | commitdiff
2014-09-10 Claudio Sacerdoti... chapter12 (coinductive) -> chapter13 tree | commitdiff
2014-08-29 Claudio Sacerdoti... Notes. tree | commitdiff
2014-08-29 Claudio Sacerdoti... A tentative chaptern on coinductive types. tree | commitdiff
2014-08-03 Andrea Aspertinew files tree | commitdiff
2014-03-07 Andrea AspertiMinor changes to make the script more robust to strateg... tree | commitdiff
2014-03-04 Claudio Sacerdoti... Inclusions improved to allow compilation from the toplevel. tree | commitdiff
2014-02-27 Claudio Sacerdoti... Porting of HOTT from Coq to Matita. tree | commitdiff
2014-01-28 Andrea AspertiAlmost there tree | commitdiff
2014-01-28 Andrea Aspertiprogress tree | commitdiff
2014-01-27 Andrea Aspertiworking version tree | commitdiff
2014-01-26 Ferruccio Guidinat: we added a non-indexed theorem tree | commitdiff
2014-01-26 Andrea Aspertimore auxiliary machines tree | commitdiff
2014-01-26 Ferruccio Guidi- nat: some additions, plus_minus_commutative renamed... tree | commitdiff
2013-12-04 Andrea AspertiNew approach: we use "iterator" steps in place of pointers. tree | commitdiff
2013-12-02 Claudio Sacerdoti... 1. more bugs fixed tree | commitdiff
2013-12-02 Claudio Sacerdoti... More progress. tree | commitdiff
2013-12-02 Claudio Sacerdoti... Some progress in the correctness proof and a bug fixed. tree | commitdiff
2013-11-29 Andrea AspertiA first example that uses a status monad where the... tree | commitdiff
2013-11-26 Ferruccio Guidi- natural numbers with infinity for lambdadelta tree | commitdiff
2013-11-25 Ferruccio Guidi- xoa: the definitions file now includes the notations... tree | commitdiff
2013-11-15 Wilmer RicciottiFinal version of the binary machine (all proofs completed). tree | commitdiff
2013-11-07 Wilmer RicciottiCloses many daemons. tree | commitdiff
2013-11-06 Wilmer RicciottiFull rework of the semantics of the binary machine... tree | commitdiff
2013-11-03 Wilmer RicciottiAlmost finished... tree | commitdiff
2013-11-03 Wilmer RicciottiMajor bugfix/reorganization/improvement of the partial... tree | commitdiff
2013-10-28 Andrea AspertiSplitted star tree | commitdiff
2013-10-25 Andrea Aspertifull.ma tree | commitdiff
2013-10-24 Andrea Aspertistep (almost) done tree | commitdiff
2013-10-24 Andrea AspertiThe step machine (draft) tree | commitdiff
2013-10-24 Andrea Aspertimany changes tree | commitdiff
2013-10-20 Wilmer RicciottiCompletes all the phases of the binary machine (modulo... tree | commitdiff
2013-10-19 Andrea AspertiSlowly porting to an enriched tape alphabet tree | commitdiff
2013-10-18 Andrea AspertiThe moves (almost) tree | commitdiff
2013-10-15 Andrea Aspertiadded sem_seq_app for the mono case tree | commitdiff
2013-10-15 Andrea Aspertirenaming files tree | commitdiff
2013-10-14 Andrea Aspertialmost there tree | commitdiff
2013-10-14 Wilmer RicciottiCompleted phases 0, 1, and 3. tree | commitdiff
2013-10-12 Andrea AspertiStill a problem to be fixed: after reaching the border... tree | commitdiff
2013-10-12 Andrea Aspertishift a trace from an extremity tree | commitdiff
2013-10-12 Andrea Aspertisplitting files tree | commitdiff
2013-10-12 Andrea AspertiMoved multi_to_mono.ma inside multi_to_mono tree | commitdiff
2013-10-09 Wilmer Ricciottiprogress in the semantics of binary machines tree | commitdiff
2013-10-07 Wilmer RicciottiStarting proof about semantics of binary machines. tree | commitdiff
2013-10-07 Wilmer RicciottiCompletes the definition of binaryTM. tree | commitdiff
2013-10-06 Andrea Aspertiprogress in the deifinition of the semantics of the... tree | commitdiff
2013-10-03 Wilmer RicciottiAdds transformation of generic monotape machines into... tree | commitdiff
2013-10-02 Andrea Aspertia vector of finsets is a finset (in progress) tree | commitdiff
2013-09-07 Ferruccio Guidisupport for nat-labeled reflexive and transitive closur... tree | commitdiff
2013-08-09 Ferruccio Guidi- we added nat-labeled reflexive and transitive closure... tree | commitdiff
2013-08-01 Ferruccio Guidipartial commit: just the components before "static... tree | commitdiff
2013-06-19 Ferruccio Guidi- partial commit :( tree | commitdiff
2013-06-05 Ferruccio Guidisome work on extended reduction ... tree | commitdiff
2013-05-31 Andrea Aspertiiteration.ma tree | commitdiff
2013-05-31 Andrea Aspertibounded quantifiers and pidgeon_hole tree | commitdiff
2013-05-31 Andrea Aspertigap.ma tree | commitdiff
2013-05-17 Andrea AspertiImproved version tree | commitdiff
2013-05-17 Andrea Aspertimore functions tree | commitdiff
2013-05-03 Andrea Aspertireverse complexity tree | commitdiff
2013-04-30 Claudio Sacerdoti... Missing include. tree | commitdiff
2013-04-30 Andrea Aspertichapter9 tree | commitdiff
2013-04-30 Andrea Aspertitutorial tree | commitdiff
2013-04-30 Claudio Sacerdoti... Old version dropped. tree | commitdiff
2013-04-30 Andrea AspertiNew notation for congruence tree | commitdiff
2013-04-30 Andrea AspertiThis line, and those below, will be ignored-- tree | commitdiff
2013-04-29 Andrea AspertiA few integrations (closed an axiom in finset). tree | commitdiff
2013-04-25 Wilmer RicciottiAn attempt at ostensiby named syntax. tree | commitdiff
2013-03-11 Andrea AspertiChpater 4 and 5 tree | commitdiff
2013-03-10 Andrea Aspertichapters 2 e 3 tree | commitdiff
2013-02-28 Ferruccio Guidi- lambdadelta: first recursive part of preservation... tree | commitdiff
2013-02-28 Andrea Aspertichapter2 revisited tree | commitdiff
2013-02-27 Andrea AspertiChapter 1 revisited tree | commitdiff
2013-02-11 Ferruccio Guidimore service lemmas in nat and lambdadelta tree | commitdiff
2013-02-07 Andrea AspertiA few integrations tree | commitdiff
2013-02-07 Andrea Aspertirestructuring tree | commitdiff
2013-02-07 Andrea Asperti(no commit message) tree | commitdiff
2013-02-07 Andrea Aspertirestructuring tree | commitdiff
2013-02-04 Wilmer Ricciottistate mte2 renamed to mte_acc tree | commitdiff
2013-02-04 Wilmer Ricciotticonverting certain basic machines to composed machines tree | commitdiff
2013-02-04 Wilmer Ricciottidefs.ma was never really used tree | commitdiff
2013-02-02 Claudio Sacerdoti... Makefile to extract to ocaml code. tree | commitdiff
2013-02-02 Claudio Sacerdoti... Oops, part of last commit (ocaml extraction implementation) tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.