2009-08-14 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Ferruccio Guidi | - xml exportation activated for the brg kernel |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | (nat,plus) is an abelian, unital magma |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Some quick patch to fix elimination that used to look for |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Assert false do not allow to debug... |
commit | commitdiff | tree | snapshot |
2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Claudio Sacerdoti... | A very little bit of arithmetic. |
commit | commitdiff | tree | snapshot |
2009-08-12 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-11 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-09 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-08 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-07 |
Ferruccio Guidi | basic_rg: improved interface, unwind removed from appli... |
commit | commitdiff | tree | snapshot |
2009-08-07 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | The first omomorphism theorem for whole sets (i.e.... |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Hmmm: I don't see much gain here. |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Metas must be handled when using iterators. |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Claudio Sacerdoti... | Setoid rewriting as unification hinting. Does not work... |
commit | commitdiff | tree | snapshot |
2009-08-06 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-05 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | More Gonthierism. Are they the right solution? |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Claudio Sacerdoti... | Hmmm, quite broken now. |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescle porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-04 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-03 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-08-01 |
Claudio Sacerdoti... | Smaller formulae. |
commit | commitdiff | tree | snapshot |
2009-08-01 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Setoids, setoids1, sets, and the like. The mess begins. |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Bad patch reverted (in error message). |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Bug fixed: one case of too many arguments was not detec... |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Serious bug fixed: uris were not refreshed when loading... |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Record projections are now defined as fixpoints in... |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | \ldots are now used in nelim and ncases |
commit | commitdiff | tree | snapshot |
2009-07-31 |
Claudio Sacerdoti... | Pp fixed in order to obtain read-back. |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | 1) \ldots here and there |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | More napply \ldots => napply |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | napply now automatically inserts \ldots at the end |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | More \ldots. |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | \ldots used here and there. Cool! |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | First implementation of \ldots. |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-30 |
Claudio Sacerdoti... | Don't reinvent the wheel. |
commit | commitdiff | tree | snapshot |
2009-07-29 |
denes | Added benchmarks |
commit | commitdiff | tree | snapshot |
2009-07-29 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-29 |
Andrea Asperti | New demodulation (innermost, optimized to avoid reducin... |
commit | commitdiff | tree | snapshot |
2009-07-29 |
Andrea Asperti | Changed the ordering of rels, and the introduction... |
commit | commitdiff | tree | snapshot |
2009-07-29 |
Andrea Asperti | Lazy strings |
commit | commitdiff | tree | snapshot |
2009-07-29 |
Andrea Asperti | Added the benchmark with the new demodulation function. |
commit | commitdiff | tree | snapshot |
2009-07-28 |
Claudio Sacerdoti... | "..." -> "\ldots" for implicit vectors |
commit | commitdiff | tree | snapshot |
2009-07-28 |
Claudio Sacerdoti... | 1) Some more work for vector implicits. |
commit | commitdiff | tree | snapshot |
2009-07-28 |
Claudio Sacerdoti... | Introduction of vectors of implicit (only for NG). |
commit | commitdiff | tree | snapshot |
2009-07-28 |
denes | New reference benchmark with CPU Time |
commit | commitdiff | tree | snapshot |
2009-07-27 |
denes | Removed meaningless time information |
commit | commitdiff | tree | snapshot |
2009-07-27 |
denes | Removed internal default timeout |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | Stupid bug fixed: the test to detect Uncertain cases... |
commit | commitdiff | tree | snapshot |
2009-07-27 |
denes | Removed old logs |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | Useless "let module" removed. |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | Since I guess the divergence bug is fixed, I activate... |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | Serious bug fixed: because of lazy evaluation of !requi... |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | setoids.ma split into setoids.ma + setoids1.ma |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | topology/igt.ma (???) |-> sets/setoids.ma |
commit | commitdiff | tree | snapshot |
2009-07-27 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-27 |
denes | Moved benchmarks to new folder |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | It works better now. |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | No more hand-made coercions. |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | Debugging code removed. |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | Record fields declared as coercions as now really decla... |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | Beta-expansion was avoided as soon as one argument... |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | Function to map NCic.term to CicNotationPt.term finished. |
commit | commitdiff | tree | snapshot |
2009-07-24 |
Claudio Sacerdoti... | Bug (found during code review) fixed (but not tested... |
commit | commitdiff | tree | snapshot |
2009-07-23 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-23 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-23 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | Elimination principles are now processed in O(1) again |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | Major speed-up: meta-chains are now expanded during... |
commit | commitdiff | tree | snapshot |
2009-07-22 |
denes | Fixed test for invertibility |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | 1) PTS simplified |
commit | commitdiff | tree | snapshot |
2009-07-22 |
denes | Now using lazy strings for debug printings |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | nelim fixed |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | leftno was List.length rights :-) |
commit | commitdiff | tree | snapshot |
2009-07-22 |
Claudio Sacerdoti... | Almost ready to implement coercion declaration for... |
commit | commitdiff | tree | snapshot |
2009-07-21 |
Cosimo Oliboni | freescale porting, work in progress |
commit | commitdiff | tree | snapshot |
2009-07-21 |
Claudio Sacerdoti... | 1) record projections are now automatically generated |
commit | commitdiff | tree | snapshot |
2009-07-21 |
Claudio Sacerdoti... | Debugging code removed. |
commit | commitdiff | tree | snapshot |
2009-07-21 |
Claudio Sacerdoti... | Record projections are now automatically generated... |
commit | commitdiff | tree | snapshot |
2009-07-21 |
denes | Implemented handling of Invertible equalities |
commit | commitdiff | tree | snapshot |
next |