| 2009-01-04 |
Claudio Sacerdoti... | Snapshot to try to understand something.
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Some more progress, fighting universe inconsistencies.
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Yet another universe problem :-(
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Back to step 1: all files that used to pass now pass...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | More re-organization.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Basic pairs went through with no problems.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Universe level fixed (litterally).
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Niceness was just a temporary illusion :-(
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Much, much nicer now.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Some more re-organization.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | More re-working.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | More reorganization.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | equivalence_relations made uniform w.r.t. universe...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Final work for today.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Some more painful work.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | binary_meet is back again, with some effort
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Many universe inconsistency avoided here and there.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | The universe inconsistency comes from big union, that...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Proof that \Omega \sup A is an overlap algebra, up...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | o-algebra defined again
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Categories and subsets compile again, hopefully with...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | WARNING: partial commit to try to understand something.
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | Some more fixes. Boring and stupid!
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | Some fixes.
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | O-Basic Topologies do form a category.
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | A few more lines.
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | Some notes by Giovanni.
|
commit | commitdiff | tree |
| 2008-12-26 |
Claudio Sacerdoti... | Some notes by Giovanni.
|
commit | commitdiff | tree |
| 2008-12-22 |
Claudio Sacerdoti... | Just copied here from formal_topologies.ma.
|
commit | commitdiff | tree |
| 2008-12-22 |
Claudio Sacerdoti... | More (ugly) work.
|
commit | commitdiff | tree |
| 2008-12-22 |
Claudio Sacerdoti... | ums got rid of
|
commit | commitdiff | tree |
| 2008-12-21 |
Claudio Sacerdoti... | 1) no more DAEMONS
|
commit | commitdiff | tree |
| 2008-12-21 |
Claudio Sacerdoti... | Using the new category SET.
|
commit | commitdiff | tree |
| 2008-12-21 |
Claudio Sacerdoti... | New category SET (whose objects are setoids).
|
commit | commitdiff | tree |
| 2008-12-18 |
Claudio Sacerdoti... | Stupid bug fixed: checkin the type in place of the...
|
commit | commitdiff | tree |
| 2008-12-18 |
Claudio Sacerdoti... | New disambiguation commented out.
|
commit | commitdiff | tree |
| 2008-12-18 |
Claudio Sacerdoti... | Many axioms are now proved... using many more (but...
|
commit | commitdiff | tree |
| 2008-12-18 |
Claudio Sacerdoti... | Now it compiles again.
|
commit | commitdiff | tree |
| 2008-12-18 |
Claudio Sacerdoti... | Refinement of axioms fixed. We did not check that the...
|
commit | commitdiff | tree |
| 2008-12-14 |
Claudio Sacerdoti... | The library is no longer automatically used during...
|
commit | commitdiff | tree |
| 2008-12-12 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-12-12 |
Claudio Sacerdoti... | A parser (and a scanner) to import "~C" files into...
|
commit | commitdiff | tree |
| 2008-12-12 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-12-12 |
Claudio Sacerdoti... | 1. new expressions AND, OR, XOR
|
commit | commitdiff | tree |
| 2008-12-11 |
Claudio Sacerdoti... | Applications are now processed from left to right.
|
commit | commitdiff | tree |
| 2008-12-08 |
Claudio Sacerdoti... | A (boring and long) once-in-a-life exercise on proving...
|
commit | commitdiff | tree |
| 2008-12-07 |
Claudio Sacerdoti... | New exception considered.
|
commit | commitdiff | tree |
| 2008-12-07 |
Claudio Sacerdoti... | Bug fixed: every time we form a Prod, we must typecheck...
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | new exception captured
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Added new syntax Type[n] where n is a number.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging code removed.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging code removed
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging instructions removed.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed.
|
commit | commitdiff | tree |
| 2008-12-05 |
Claudio Sacerdoti... | Case-sensitive fixes.
|
commit | commitdiff | tree |
| 2008-12-03 |
Claudio Sacerdoti... | The aliases and multi_aliases in the lexicon status...
|
commit | commitdiff | tree |
| 2008-12-01 |
Claudio Sacerdoti... | rt.op and check.opt removed from Makefile
|
commit | commitdiff | tree |
| 2008-11-27 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-11-27 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-11-27 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-11-15 |
Claudio Sacerdoti... | New bug.
|
commit | commitdiff | tree |
| 2008-11-15 |
Claudio Sacerdoti... | Another bug.
|
commit | commitdiff | tree |
| 2008-11-15 |
Claudio Sacerdoti... | This commit shows a bug.
|
commit | commitdiff | tree |
| 2008-11-11 |
Claudio Sacerdoti... | 1. data structure for lables is now more strict
|
commit | commitdiff | tree |
| 2008-11-09 |
Claudio Sacerdoti... | auto-param "size" missing
|
commit | commitdiff | tree |
| 2008-11-06 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-11-06 |
Claudio Sacerdoti... | First attempts at the third phase.
|
commit | commitdiff | tree |
| 2008-11-04 |
Claudio Sacerdoti... | - A new interesting elimination principle over inductively...
|
commit | commitdiff | tree |
| 2008-10-31 |
Claudio Sacerdoti... | Environment simplified.
|
commit | commitdiff | tree |
| 2008-10-31 |
Claudio Sacerdoti... | No longer used.
|
commit | commitdiff | tree |
| 2008-10-31 |
Claudio Sacerdoti... | - New dependency for environments on the nesting depth.
|
commit | commitdiff | tree |
| 2008-10-16 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-10-15 |
Claudio Sacerdoti... | minor simplification + deps fixed
|
commit | commitdiff | tree |
| 2008-10-15 |
Claudio Sacerdoti... | New invariant and data structure to represent environments...
|
commit | commitdiff | tree |
| 2008-10-13 |
Claudio Sacerdoti... | Bug fixed in LetIn: the cumulativity test was performed...
|
commit | commitdiff | tree |
| 2008-10-01 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-10-01 |
Claudio Sacerdoti... | - setters for data structures now support "commuting...
|
commit | commitdiff | tree |
| 2008-09-25 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-09-25 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-09-18 |
Claudio Sacerdoti... | ppterm_in_named_context removed in favour of the high...
|
commit | commitdiff | tree |
| 2008-09-18 |
Claudio Sacerdoti... | Major reordering of theorems in the appropriate files.
|
commit | commitdiff | tree |
| 2008-09-18 |
Claudio Sacerdoti... | In case of coercion to Prod, the error message shown...
|
commit | commitdiff | tree |
| 2008-09-18 |
Claudio Sacerdoti... | Precedence level of \downarrow changed to match that...
|
commit | commitdiff | tree |
| 2008-09-16 |
Claudio Sacerdoti... | formal_map now defined
|
commit | commitdiff | tree |
| 2008-09-16 |
Claudio Sacerdoti... | Definition of formal_topologies.
|
commit | commitdiff | tree |
| 2008-09-15 |
Claudio Sacerdoti... | BTop is a category.
|
commit | commitdiff | tree |
| 2008-09-12 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-09-12 |
Claudio Sacerdoti... | 1) as usual, I took the reverse notation for composition.
|
commit | commitdiff | tree |
| 2008-09-11 |
Claudio Sacerdoti... | helm mailing list moved to cs.unibo.it
|
commit | commitdiff | tree |
| 2008-09-09 |
Claudio Sacerdoti... | Reordering of lemmas in proper places.
|
commit | commitdiff | tree |
| 2008-09-09 |
Claudio Sacerdoti... | Concrete spaces do form a category, after all :-)
|
commit | commitdiff | tree |
| 2008-09-09 |
Claudio Sacerdoti... | Getting closer thanks to more technical arrangements.
|
commit | commitdiff | tree |
| 2008-09-08 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-09-08 |
Claudio Sacerdoti... | Concrete spaces now defined.
|
commit | commitdiff | tree |
| 2008-09-08 |
Claudio Sacerdoti... | Case c1 t1 vs c2 t2 where c1 and c2 are not splitted...
|
commit | commitdiff | tree |
| 2008-09-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-09-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search