| 2009-08-20 | 
Claudio Sacerdoti...  | - Bug fixed in definition of big_op. | 
commit | commitdiff | tree | snapshot | 
| 2009-08-20 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-20 | 
Ferruccio Guidi | - sort inclusion must be restricted to term backbone...  | 
commit | commitdiff | tree | snapshot | 
| 2009-08-19 | 
Claudio Sacerdoti...  | One half done. | 
commit | commitdiff | tree | snapshot | 
| 2009-08-19 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-18 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-18 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-18 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-17 | 
Ferruccio Guidi | - alpha conversion check added to the brg kernel (succe...  | 
commit | commitdiff | tree | snapshot | 
| 2009-08-16 | 
Ferruccio Guidi | - performance data added for reference | 
commit | commitdiff | tree | snapshot | 
| 2009-08-16 | 
Ferruccio Guidi | - proper KAM with closures implemented for the brg...  | 
commit | commitdiff | tree | snapshot | 
| 2009-08-15 | 
Ferruccio Guidi | - kernel parameters indication added to exported object...  | 
commit | commitdiff | tree | snapshot | 
| 2009-08-14 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-14 | 
Claudio Sacerdoti...  | ... | 
commit | commitdiff | tree | snapshot | 
| 2009-08-14 | 
Claudio Sacerdoti...  | Since the introduction of saturation, an assert false...  | 
commit | commitdiff | tree | snapshot | 
| 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 | 
| next |