]> 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
- the relation for pointwise extensions now takes a binder as argument
[helm.git] / matita / matita / lib /
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
2013-02-01 Ferruccio Guidilambda finaly moved in lib tree | commitdiff
2013-02-01 Wilmer Ricciottimatch now only uses the new move operation tree | commitdiff
2013-01-29 Wilmer RicciottiSpeed-up in match.ma. tree | commitdiff
2013-01-29 Wilmer RicciottiProved old axiom. tree | commitdiff
2013-01-29 Wilmer RicciottiYippeee! Completes proof of soundness of the universal... tree | commitdiff
2013-01-28 Andrea Aspertiunistep!!! tree | commitdiff
2013-01-28 Andrea Aspertifunzioni ausiliarie tree | commitdiff
2013-01-28 Wilmer Ricciotticfg_in_table_to_tuple tree | commitdiff
2013-01-28 Wilmer Ricciottisem_copy_strict tree | commitdiff
2013-01-27 Wilmer Ricciottimany axioms and daemons removed tree | commitdiff
2013-01-27 Andrea Aspertiquasi finito tree | commitdiff
2013-01-27 Wilmer Ricciottiwell-foundedness done tree | commitdiff
2013-01-27 Andrea Aspertisem_exec_move completed tree | commitdiff
2013-01-27 Andrea Aspertialmost there tree | commitdiff
2013-01-26 Andrea AspertiA lot of changes tree | commitdiff
2013-01-25 Andrea AspertiSplitted unistep_aux tree | commitdiff
2013-01-25 Wilmer Ricciottistarted unistep tree | commitdiff
2013-01-25 Wilmer Ricciottiprogress in termination tree | commitdiff
2013-01-24 Wilmer Ricciottifinished semantics for termination of match machine tree | commitdiff
2013-01-24 Wilmer Ricciottiprogress tree | commitdiff
2013-01-24 Wilmer Ricciottiprogress tree | commitdiff
2013-01-23 Wilmer Ricciottiprogress tree | commitdiff
2013-01-22 Andrea Aspertitermination! tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.