]> matita.cs.unibo.it Git - helm.git/shortlog
projects / helm.git / shortlog
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
helm.git
2009-01-06 Claudio Sacerdoti... The functor from BP to OBP has been defined (but no... commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... Ok, even if not stated formally, now we know that the... commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... orelation_of_relation preserves equality and identities. commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... Basic pairs restored; require renaming to use them... commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... Some progress: everything works well now. commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... Ooops, I forgot to commit this in the previous 3-4... commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... An hint moved to the right place. commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... No more daemons, no more exTs. commit | commitdiff | tree | snapshot
2009-01-06 Claudio Sacerdoti... Great: some significant progress in fixing universe... commit | commitdiff | tree | snapshot
2009-01-05 Enrico Tassiremoving (only from the interface) functions related... commit | commitdiff | tree | snapshot
2009-01-05 Enrico Tassiadded help on virtuals and UTF-8 equivalence classes commit | commitdiff | tree | snapshot
2009-01-05 Enrico Tassiexpand ligatures after \n too commit | commitdiff | tree | snapshot
2009-01-05 Enrico Tassiadded := -> \def commit | commitdiff | tree | snapshot
2009-01-05 Enrico Tassiadded some memory to virtuals eq classes commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... 1. CProp_n fixed to be equal to Type_n to better unders... commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... Snapshot to try to understand something. commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... Some more progress, fighting universe inconsistencies. commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... Yet another universe problem :-( commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... ... commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... Back to step 1: all files that used to pass now pass... commit | commitdiff | tree | snapshot
2009-01-04 Claudio Sacerdoti... More re-organization. commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... Basic pairs went through with no problems. commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... Universe level fixed (litterally). commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... Niceness was just a temporary illusion :-( commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... Much, much nicer now. commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... Some more re-organization. commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... More re-working. commit | commitdiff | tree | snapshot
2009-01-03 Claudio Sacerdoti... More reorganization. commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... equivalence_relations made uniform w.r.t. universe... commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... Final work for today. commit | commitdiff | tree | snapshot
2008-12-28 Enrico Tassiremoved duplicate notation commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... Some more painful work. commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... binary_meet is back again, with some effort commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... Many universe inconsistency avoided here and there. commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... The universe inconsistency comes from big union, that... commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... Proof that \Omega \sup A is an overlap algebra, up... commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... o-algebra defined again commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... Categories and subsets compile again, hopefully with... commit | commitdiff | tree | snapshot
2008-12-28 Claudio Sacerdoti... WARNING: partial commit to try to understand something. commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... Some more fixes. Boring and stupid! commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... Some fixes. commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... O-Basic Topologies do form a category. commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... A few more lines. commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni. commit | commitdiff | tree | snapshot
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni. commit | commitdiff | tree | snapshot
2008-12-24 Enrico Tassiadded some virtuals commit | commitdiff | tree | snapshot
2008-12-24 Enrico Tassibug fixed, all convertible was called without a metasenv commit | commitdiff | tree | snapshot
2008-12-22 Claudio Sacerdoti... Just copied here from formal_topologies.ma. commit | commitdiff | tree | snapshot
2008-12-22 Claudio Sacerdoti... More (ugly) work. commit | commitdiff | tree | snapshot
2008-12-22 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-22 Enrico TassiBeginning of o-basic_topologies. commit | commitdiff | tree | snapshot
2008-12-22 Enrico TassiSome clean up. commit | commitdiff | tree | snapshot
2008-12-22 Enrico TassiConcrete Spaces defined but... they require about 20m... commit | commitdiff | tree | snapshot
2008-12-22 Enrico Tassi1 more lemma commit | commitdiff | tree | snapshot
2008-12-22 Enrico Tassione line commit | commitdiff | tree | snapshot
2008-12-22 Enrico Tassisome work commit | commitdiff | tree | snapshot
2008-12-22 Claudio Sacerdoti... ums got rid of commit | commitdiff | tree | snapshot
2008-12-21 Claudio Sacerdoti... 1) no more DAEMONS commit | commitdiff | tree | snapshot
2008-12-21 Enrico Tassimerged commits, the same proof is missing :-( commit | commitdiff | tree | snapshot
2008-12-21 Enrico Tassibleah commit | commitdiff | tree | snapshot
2008-12-21 Claudio Sacerdoti... Using the new category SET. commit | commitdiff | tree | snapshot
2008-12-21 Claudio Sacerdoti... New category SET (whose objects are setoids). commit | commitdiff | tree | snapshot
2008-12-20 Ferruccio Guidiwe started the support for naive sort inclusion commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassibetter pp of virtuals commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassimore pps commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassitype3 commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiranking hopefully fixed commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassifix exponentiation commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassigo notation go! commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassifixed, it seems the new handling of hints in some rare... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiadded aliases for _ and fixed greek leters thanks to... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassibetter pps commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassihandles bad Appl commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiadded better debug_pps and add_user_provided_unificatio... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiadded unification hint commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiunification hint commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassilambda case fixed, used to not properly use the expecte... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiadded 'unification hint command to add a term to the... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassiidentity coercions are not really inserted, just used... commit | commitdiff | tree | snapshot
2008-12-19 Enrico Tassi.... commit | commitdiff | tree | snapshot
2008-12-18 Claudio Sacerdoti... Stupid bug fixed: checkin the type in place of the... commit | commitdiff | tree | snapshot
2008-12-18 Claudio Sacerdoti... New disambiguation commented out. commit | commitdiff | tree | snapshot
2008-12-18 Claudio Sacerdoti... Many axioms are now proved... using many more (but... commit | commitdiff | tree | snapshot
2008-12-18 Claudio Sacerdoti... Now it compiles again. commit | commitdiff | tree | snapshot
2008-12-18 Claudio Sacerdoti... Refinement of axioms fixed. We did not check that the... commit | commitdiff | tree | snapshot
2008-12-18 Ferruccio Guidi- improved logging commit | commitdiff | tree | snapshot
2008-12-18 Enrico Tassi... commit | commitdiff | tree | snapshot
2008-12-17 Ferruccio Guidiwe started the support for the coercions "alle" and... commit | commitdiff | tree | snapshot
2008-12-17 Enrico Tassifoo overlap commit | commitdiff | tree | snapshot
2008-12-17 Enrico Tassifoo overlap commit | commitdiff | tree | snapshot
2008-12-17 Enrico Tassi.... commit | commitdiff | tree | snapshot
2008-12-16 Ferruccio Guidiwe added the implicit coercion for modus tollens commit | commitdiff | tree | snapshot
2008-12-16 Enrico Tassiprevious change was causing divergence commit | commitdiff | tree | snapshot
next
Unnamed repository; edit this file 'description' to name the repository.