| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
tree | commitdiff |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-03-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-03-12 |
Claudio Sacerdoti... | More details on the proof. |
tree | commitdiff |
| 2009-03-12 |
Claudio Sacerdoti... | New algorithm based on in-place modification of the... |
tree | commitdiff |
| 2009-03-06 |
Claudio Sacerdoti... | Minor improvements in pretty-printing. |
tree | commitdiff |
| 2009-03-05 |
Claudio Sacerdoti... | New version: only new nodes are normalized; moreover... |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | New version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | First version. |
tree | commitdiff |
| 2009-03-02 |
Claudio Sacerdoti... | Old algorithm moved to old to leave place to the new... |
tree | commitdiff |
| 2009-02-06 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-02-03 |
Enrico Tassi | some work to speed up the system |
tree | commitdiff |
| 2009-02-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-02-02 |
Claudio Sacerdoti... | Hmmm, going too low. |
tree | commitdiff |
| 2009-02-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-02-01 |
Claudio Sacerdoti... | Towards fullness. |
tree | commitdiff |
| 2009-02-01 |
Claudio Sacerdoti... | Renaming. |
tree | commitdiff |
| 2009-02-01 |
Claudio Sacerdoti... | Renaming. |
tree | commitdiff |
| 2009-01-29 |
Enrico Tassi | more polishing |
tree | commitdiff |
| 2009-01-29 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | some work |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-01-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-01-26 |
Enrico Tassi | minor fixes |
tree | commitdiff |
| 2009-01-22 |
Claudio Sacerdoti... | TODO |
tree | commitdiff |
| 2009-01-21 |
Enrico Tassi | some minor fixes |
tree | commitdiff |
| 2009-01-21 |
Enrico Tassi | a bit of work done while travelling to padova |
tree | commitdiff |
| 2009-01-19 |
Enrico Tassi | - new notation.ma file with local and common notation |
tree | commitdiff |
| 2009-01-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-01-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many... |
tree | commitdiff |
| 2009-01-18 |
Claudio Sacerdoti... | universe inconsistency fixed |
tree | commitdiff |
| 2009-01-18 |
Claudio Sacerdoti... | SUBSETS_full up to universe inconsistency |
tree | commitdiff |
| 2009-01-17 |
Claudio Sacerdoti... | faithful |
tree | commitdiff |
| 2009-01-17 |
Claudio Sacerdoti... | CAT2 |
tree | commitdiff |
| 2009-01-16 |
Claudio Sacerdoti... | Sambin's result holds trivially since most of the field... |
tree | commitdiff |
| 2009-01-16 |
Claudio Sacerdoti... | basic topologies are trivially o-basic topologies |
tree | commitdiff |
| 2009-01-16 |
Claudio Sacerdoti... | 1. new coercion(s) from CPropi to CProp |
tree | commitdiff |
| 2009-01-15 |
Enrico Tassi | the new coercion behaviour (variants + composition... |
tree | commitdiff |
| 2009-01-14 |
Claudio Sacerdoti... | o_continous_relations are really o_relation_pair..... |
tree | commitdiff |
| 2009-01-14 |
Claudio Sacerdoti... | o-basic_pairs are indeed examples of o-basic_topologies! |
tree | commitdiff |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
| 2009-01-12 |
Claudio Sacerdoti... | Some work on o-algebras towards the proof that a and... |
tree | commitdiff |
| 2009-01-08 |
Claudio Sacerdoti... | The new coercion from SET to Type0 with higher priority... |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | more composites to make all happy! |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | eq over SET1 and SET no longer used |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | some more if/fi conversion due to the new . binding |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | unary_morphism_N : seoidN -> setoidN -> setoidN (was... |
tree | commitdiff |
| 2009-01-08 |
Claudio Sacerdoti... | Just a snapshot. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | More work on concrete spaces. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Some work on concrete spaces. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Cool: only 8 universes in use. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | 1) Some reorganization. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Some renaming to avoid confusion between saturations... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Fixing universe levels for saturations and (partially... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | The functor from BP to OBP has been defined (but no... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Ok, even if not stated formally, now we know that the... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | orelation_of_relation preserves equality and identities. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Basic pairs restored; require renaming to use them... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Some progress: everything works well now. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Ooops, I forgot to commit this in the previous 3-4... |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | An hint moved to the right place. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | No more daemons, no more exTs. |
tree | commitdiff |
| 2009-01-06 |
Claudio Sacerdoti... | Great: some significant progress in fixing universe... |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | 1. CProp_n fixed to be equal to Type_n to better unders... |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | Snapshot to try to understand something. |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | Some more progress, fighting universe inconsistencies. |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | Yet another universe problem :-( |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | Back to step 1: all files that used to pass now pass... |
tree | commitdiff |
| 2009-01-04 |
Claudio Sacerdoti... | More re-organization. |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | Basic pairs went through with no problems. |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | Universe level fixed (litterally). |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | Niceness was just a temporary illusion :-( |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | Much, much nicer now. |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | Some more re-organization. |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | More re-working. |
tree | commitdiff |
| 2009-01-03 |
Claudio Sacerdoti... | More reorganization. |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | equivalence_relations made uniform w.r.t. universe... |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | Final work for today. |
tree | commitdiff |
| 2008-12-28 |
Enrico Tassi | removed duplicate notation |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | Some more painful work. |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | binary_meet is back again, with some effort |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | Many universe inconsistency avoided here and there. |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | The universe inconsistency comes from big union, that... |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | Proof that \Omega \sup A is an overlap algebra, up... |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | o-algebra defined again |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | Categories and subsets compile again, hopefully with... |
tree | commitdiff |
| 2008-12-28 |
Claudio Sacerdoti... | WARNING: partial commit to try to understand something. |
tree | commitdiff |
| 2008-12-26 |
Claudio Sacerdoti... | Some more fixes. Boring and stupid! |
tree | commitdiff |
| next |
projects / helm.git / history