]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2009-08-04 Cosimo Oliboni freescle porting, work in progress
2009-08-04 Cosimo Oliboni freescale porting, work in progress
2009-08-03 Cosimo Oliboni freescale porting, work in progress
2009-08-01 Claudio Sacerdoti... Smaller formulae.
2009-08-01 Cosimo Oliboni freescale porting, work in progress
2009-07-31 Cosimo Oliboni freescale porting, work in progress
2009-07-31 Claudio Sacerdoti... Setoids, setoids1, sets, and the like. The mess begins.
2009-07-31 Claudio Sacerdoti... Bad patch reverted (in error message).
2009-07-31 Claudio Sacerdoti... Bug fixed: one case of too many arguments was not detec...
2009-07-31 Claudio Sacerdoti... Serious bug fixed: uris were not refreshed when loading...
2009-07-31 Claudio Sacerdoti... Record projections are now defined as fixpoints in...
2009-07-31 Claudio Sacerdoti... \ldots are now used in nelim and ncases
2009-07-31 Claudio Sacerdoti... Pp fixed in order to obtain read-back.
2009-07-30 Claudio Sacerdoti... 1) \ldots here and there
2009-07-30 Claudio Sacerdoti... More napply \ldots => napply
2009-07-30 Claudio Sacerdoti... napply now automatically inserts \ldots at the end
2009-07-30 Claudio Sacerdoti... More \ldots.
2009-07-30 Claudio Sacerdoti... \ldots used here and there. Cool!
2009-07-30 Claudio Sacerdoti... First implementation of \ldots.
2009-07-30 Claudio Sacerdoti... ...
2009-07-30 Claudio Sacerdoti... Don't reinvent the wheel.
2009-07-29 denesAdded benchmarks
2009-07-29 Cosimo Oliboni freescale porting, work in progress
2009-07-29 Andrea AspertiNew demodulation (innermost, optimized to avoid reducin...
2009-07-29 Andrea AspertiChanged the ordering of rels, and the introduction...
2009-07-29 Andrea AspertiLazy strings
2009-07-29 Andrea AspertiAdded the benchmark with the new demodulation function.
2009-07-28 Claudio Sacerdoti... "..." -> "\ldots" for implicit vectors
2009-07-28 Claudio Sacerdoti... 1) Some more work for vector implicits.
2009-07-28 Claudio Sacerdoti... Introduction of vectors of implicit (only for NG).
2009-07-28 denesNew reference benchmark with CPU Time
2009-07-27 denesRemoved meaningless time information
2009-07-27 denesRemoved internal default timeout
2009-07-27 Claudio Sacerdoti... Stupid bug fixed: the test to detect Uncertain cases...
2009-07-27 denesRemoved old logs
2009-07-27 Claudio Sacerdoti... Useless "let module" removed.
2009-07-27 Claudio Sacerdoti... Since I guess the divergence bug is fixed, I activate...
2009-07-27 Claudio Sacerdoti... Serious bug fixed: because of lazy evaluation of !requi...
2009-07-27 Claudio Sacerdoti... setoids.ma split into setoids.ma + setoids1.ma
2009-07-27 Claudio Sacerdoti... topology/igt.ma (???) |-> sets/setoids.ma
2009-07-27 Claudio Sacerdoti... ...
2009-07-27 denesMoved benchmarks to new folder
2009-07-24 Claudio Sacerdoti... It works better now.
2009-07-24 Claudio Sacerdoti... ...
2009-07-24 Claudio Sacerdoti... No more hand-made coercions.
2009-07-24 Claudio Sacerdoti... Debugging code removed.
2009-07-24 Claudio Sacerdoti... Record fields declared as coercions as now really decla...
2009-07-24 Claudio Sacerdoti... Beta-expansion was avoided as soon as one argument...
2009-07-24 Claudio Sacerdoti... ...
2009-07-24 Claudio Sacerdoti... Function to map NCic.term to CicNotationPt.term finished.
2009-07-24 Claudio Sacerdoti... Bug (found during code review) fixed (but not tested...
2009-07-23 Claudio Sacerdoti... ...
2009-07-23 Cosimo Oliboni freescale porting, work in progress
2009-07-23 Cosimo Oliboni freescale porting, work in progress
2009-07-22 Claudio Sacerdoti... Elimination principles are now processed in O(1) again
2009-07-22 Claudio Sacerdoti... Major speed-up: meta-chains are now expanded during...
2009-07-22 denesFixed test for invertibility
2009-07-22 Claudio Sacerdoti... ...
2009-07-22 Claudio Sacerdoti... 1) PTS simplified
2009-07-22 denesNow using lazy strings for debug printings
2009-07-22 Claudio Sacerdoti... ...
2009-07-22 Claudio Sacerdoti... nelim fixed
2009-07-22 Claudio Sacerdoti... leftno was List.length rights :-)
2009-07-22 Claudio Sacerdoti... Almost ready to implement coercion declaration for...
2009-07-21 Cosimo Oliboni freescale porting, work in progress
2009-07-21 Claudio Sacerdoti... 1) record projections are now automatically generated
2009-07-21 Claudio Sacerdoti... Debugging code removed.
2009-07-21 Claudio Sacerdoti... Record projections are now automatically generated...
2009-07-21 denesImplemented handling of Invertible equalities
2009-07-20 Enrico Tassisorted modules
2009-07-20 Claudio Sacerdoti... Debugging printf removed
2009-07-20 Claudio Sacerdoti... nrewrite now uses the appropriate principle when going...
2009-07-20 Claudio Sacerdoti... nrewrite now working
2009-07-20 Claudio Sacerdoti... ...
2009-07-20 denesRemoved status printing by processes
2009-07-20 denesFixed multiple printing
2009-07-20 Wilmer RicciottiFinal version, submitted to CASC-22.
2009-07-20 Wilmer Ricciottiadded a flag for age selection
2009-07-20 Claudio Sacerdoti... Very serious bug fixed in unification, but the fix...
2009-07-20 Claudio Sacerdoti... 1) The NG kernel now accepts only usage of declared...
2009-07-20 denesOne-side indexing for commutativity
2009-07-20 denesNo demod call on functionnal symbols
2009-07-20 Claudio Sacerdoti... 1) ppmetasenv and ppcontext to reduce the amount of...
2009-07-19 Cosimo Oliboni freescale porting, work in progress
2009-07-17 Claudio Sacerdoti... ...
2009-07-17 Claudio Sacerdoti... nelim now uses the appropriate _rect_XXX elimination...
2009-07-17 Claudio Sacerdoti... 1) the user is notified when a new object is defined
2009-07-17 Claudio Sacerdoti... More info to refine empty types elimination.
2009-07-17 Claudio Sacerdoti... Old code commented out.
2009-07-17 Claudio Sacerdoti... Generation of principles is now atomic.
2009-07-17 Claudio Sacerdoti... Debugging code commented out.
2009-07-17 Enrico Tassiadd comment
2009-07-17 Claudio Sacerdoti... Non reproducible.
2009-07-17 Claudio Sacerdoti... Some bugs already fixed.
2009-07-17 Claudio Sacerdoti... Bugs (mostly from Oliboni)
2009-07-17 Claudio Sacerdoti... Bug fixed: singleton application.
2009-07-17 Claudio Sacerdoti... New suffixes for elimination principles:
2009-07-17 Claudio Sacerdoti... 1) added a function to retrieve all the universes curre...
2009-07-17 Cosimo Oliboni freescale porting, work in progress
2009-07-17 Claudio Sacerdoti... Generation of inductive principle for Type[0].
next