2009-02-15 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-02-15 |
Enrico Tassi | commented some printings |
commit | commitdiff | tree | snapshot |
2009-02-15 |
Enrico Tassi | minor changes to make the library compile after wilmers... |
commit | commitdiff | tree | snapshot |
2009-02-13 |
Wilmer Ricciotti | Axiomatization of real numbers (work in progress) |
commit | commitdiff | tree | snapshot |
2009-02-12 |
Andrea Asperti | errata corrige. |
commit | commitdiff | tree | snapshot |
2009-02-12 |
Andrea Asperti | Fixed a problem of lifting. |
commit | commitdiff | tree | snapshot |
2009-02-11 |
Enrico Tassi | some work to refine objs |
commit | commitdiff | tree | snapshot |
2009-02-11 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-02-09 |
Enrico Tassi | b:action are now considered as m:maction and thus are... |
commit | commitdiff | tree | snapshot |
2009-02-06 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-02-05 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-02-05 |
Enrico Tassi | a non necessary but morally required change. The matche... |
commit | commitdiff | tree | snapshot |
2009-02-03 |
Enrico Tassi | some work to speed up the system |
commit | commitdiff | tree | snapshot |
2009-02-03 |
Enrico Tassi | case tactic first tries with a simple outtype and then... |
commit | commitdiff | tree | snapshot |
2009-02-02 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-02-02 |
Enrico Tassi | CicTypeChecker.typecheck now takes an additional parameter: |
commit | commitdiff | tree | snapshot |
2009-02-02 |
Claudio Sacerdoti... | Hmmm, going too low. |
commit | commitdiff | tree | snapshot |
2009-02-02 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-02-01 |
Claudio Sacerdoti... | Towards fullness. |
commit | commitdiff | tree | snapshot |
2009-02-01 |
Claudio Sacerdoti... | Renaming. |
commit | commitdiff | tree | snapshot |
2009-02-01 |
Claudio Sacerdoti... | Renaming. |
commit | commitdiff | tree | snapshot |
2009-01-30 |
Enrico Tassi | fix convertibility in case of application test_eq_only... |
commit | commitdiff | tree | snapshot |
2009-01-29 |
Enrico Tassi | more polishing |
commit | commitdiff | tree | snapshot |
2009-01-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-29 |
Enrico Tassi | application arguments are compared with test_eq_only... |
commit | commitdiff | tree | snapshot |
2009-01-28 |
Enrico Tassi | some work |
commit | commitdiff | tree | snapshot |
2009-01-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-27 |
Enrico Tassi | maction, mpadded and mstyle added to documentation |
commit | commitdiff | tree | snapshot |
2009-01-26 |
Enrico Tassi | minor fixes |
commit | commitdiff | tree | snapshot |
2009-01-26 |
Enrico Tassi | maction support added to notation, adopted for = AKA... |
commit | commitdiff | tree | snapshot |
2009-01-26 |
Enrico Tassi | maction layout added to notation |
commit | commitdiff | tree | snapshot |
2009-01-26 |
Enrico Tassi | we were generating a name for the main fix twice |
commit | commitdiff | tree | snapshot |
2009-01-26 |
Enrico Tassi | added a number to identical error messages to ease... |
commit | commitdiff | tree | snapshot |
2009-01-23 |
Ferruccio Guidi | OEIS sequence identifier found for P(n) |
commit | commitdiff | tree | snapshot |
2009-01-22 |
Claudio Sacerdoti... | TODO |
commit | commitdiff | tree | snapshot |
2009-01-21 |
Enrico Tassi | some minor fixes |
commit | commitdiff | tree | snapshot |
2009-01-21 |
Enrico Tassi | a bit of work done while travelling to padova |
commit | commitdiff | tree | snapshot |
2009-01-19 |
Enrico Tassi | - new notation.ma file with local and common notation |
commit | commitdiff | tree | snapshot |
2009-01-19 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-01-19 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many... |
commit | commitdiff | tree | snapshot |
2009-01-18 |
Claudio Sacerdoti... | universe inconsistency fixed |
commit | commitdiff | tree | snapshot |
2009-01-18 |
Claudio Sacerdoti... | SUBSETS_full up to universe inconsistency |
commit | commitdiff | tree | snapshot |
2009-01-17 |
Claudio Sacerdoti... | faithful |
commit | commitdiff | tree | snapshot |
2009-01-17 |
Claudio Sacerdoti... | CAT2 |
commit | commitdiff | tree | snapshot |
2009-01-16 |
Enrico Tassi | ceommented out metasenv |
commit | commitdiff | tree | snapshot |
2009-01-16 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2009-01-16 |
Claudio Sacerdoti... | Sambin's result holds trivially since most of the field... |
commit | commitdiff | tree | snapshot |
2009-01-16 |
Claudio Sacerdoti... | basic topologies are trivially o-basic topologies |
commit | commitdiff | tree | snapshot |
2009-01-16 |
Claudio Sacerdoti... | 1. new coercion(s) from CPropi to CProp |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | the new coercion behaviour (variants + composition... |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | added notation for 'Vdash |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | if the user attempts to insert a duplicate coercions... |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | unvariant also for coercions to funclass |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | - name mangling changed, added __ to separate additiona... |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | no more universe inconsistency printed to stderr |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | coercions that are marked as variant are unfolded when... |
commit | commitdiff | tree | snapshot |
2009-01-15 |
Enrico Tassi | Coercions graph is printed between real types and not... |
commit | commitdiff | tree | snapshot |
2009-01-14 |
Claudio Sacerdoti... | o_continous_relations are really o_relation_pair..... |
commit | commitdiff | tree | snapshot |
2009-01-14 |
Claudio Sacerdoti... | o-basic_pairs are indeed examples of o-basic_topologies! |
commit | commitdiff | tree | snapshot |
2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
commit | commitdiff | tree | snapshot |
2009-01-13 |
Claudio Sacerdoti... | - Added new output in standard C. |
commit | commitdiff | tree | snapshot |
2009-01-12 |
Claudio Sacerdoti... | Some work on o-algebras towards the proof that a and... |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Claudio Sacerdoti... | The new coercion from SET to Type0 with higher priority... |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Enrico Tassi | more composites to make all happy! |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Enrico Tassi | eq over SET1 and SET no longer used |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Enrico Tassi | some more if/fi conversion due to the new . binding |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Enrico Tassi | unary_morphism_N : seoidN -> setoidN -> setoidN (was... |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Enrico Tassi | virtuals for () removed and bound to 'o' |
commit | commitdiff | tree | snapshot |
2009-01-08 |
Claudio Sacerdoti... | Just a snapshot. |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Enrico Tassi | coercions reordering implemented |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Enrico Tassi | updated |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | More work on concrete spaces. |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | Some work on concrete spaces. |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | Cool: only 8 universes in use. |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | 1) Some reorganization. |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | Some renaming to avoid confusion between saturations... |
commit | commitdiff | tree | snapshot |
2009-01-06 |
Claudio Sacerdoti... | Fixing universe levels for saturations and (partially... |
commit | commitdiff | tree | snapshot |
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 Tassi | removing (only from the interface) functions related... |
commit | commitdiff | tree | snapshot |
2009-01-05 |
Enrico Tassi | added help on virtuals and UTF-8 equivalence classes |
commit | commitdiff | tree | snapshot |
2009-01-05 |
Enrico Tassi | expand ligatures after \n too |
commit | commitdiff | tree | snapshot |
2009-01-05 |
Enrico Tassi | added := -> \def |
commit | commitdiff | tree | snapshot |
2009-01-05 |
Enrico Tassi | added 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 |
next |