]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
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].
2009-07-16 Cosimo Oliboni freescale porting, work in progress
2009-07-16 denesSorted version of eligible problems list
2009-07-16 denesDisabled age selection and ad hoc goal weight computation
2009-07-15 Enrico Tassincopy partially implemented and fixed (a ?) chain to...
2009-07-15 Wilmer RicciottiFixed dependency function, which was lacking the code...
2009-07-15 Enrico Tassi...
2009-07-15 Enrico Tassimatch_coercion gives back the saturations, not the...
2009-07-15 Cosimo Oliboni freescale porting, work in progress
2009-07-14 denesFixed Option type error (OCaml bug)
2009-07-14 denes.
2009-07-14 denes.
2009-07-14 Cosimo Oliboni freescale porting to ng, work in progress
2009-07-13 Enrico Tassibetter spacing
2009-07-13 Enrico Tassistatistics are used, when possible, to sort
2009-07-13 denesAdded statistics printings
2009-07-13 denesAdded statistics module
2009-07-13 Claudio Sacerdoti... First proof finished (some tactics still not working).
2009-07-13 Enrico Tassimatitaprover is now flexible enough to allow the comput...
2009-07-13 Claudio Sacerdoti... Coercion hiding implemented. Notes:
2009-07-13 Cosimo Oliboni freescale translation (work in progress)
2009-07-12 Cosimo Oliboni(no commit message)
2009-07-11 Cosimo Oliboni(no commit message)
2009-07-10 Claudio Sacerdoti... Composite coercions are here!
2009-07-10 Ferruccio Guidi- brgOutput: the nodes count is now implemented
2009-07-10 Enrico Tassiinitial implementation of coercion composition
2009-07-10 Enrico Tassimore work on coercions composition
2009-07-10 Cosimo Oliboni +root +depends
2009-07-10 denesRemoved unused parameter of unification procedure ...
2009-07-10 Enrico Tassimore profilers
2009-07-10 Claudio Sacerdoti... Coercions used here and there.
2009-07-10 Claudio Sacerdoti... Bug fixed (missing ctx) + comment added.
2009-07-10 Claudio Sacerdoti... ...
2009-07-10 Cosimo Oliboninew ng freescale, no external dependencies
2009-07-10 Claudio Sacerdoti... Let's live with new ocaml type system limitations...
2009-07-09 Enrico Tassiinitial implementation of `ncoercion name : type :...
2009-07-09 Enrico Tassiclaudio, please have a look at this
2009-07-09 Enrico Tassinew nrepeat (and block '('...')' ) tactical
2009-07-09 Enrico Tassi...
2009-07-09 Enrico TassiNew functorialization: paramod is abstracted over a...
2009-07-09 denesFixed check for condition iv p.33 (Riazzanov)
2009-07-09 Wilmer RicciottiMore updates to Fsub.
2009-07-09 Enrico Tassiprofile most operations, do not return a filtered varli...
2009-07-09 Enrico Tassi1 process for now
2009-07-09 Enrico Tassitwo cases should be assert false at least in TPTP
2009-07-09 Enrico Tassimicro optimizations to unification
2009-07-09 denesCleaned a bit
2009-07-09 Enrico Tassi...
2009-07-09 Enrico Tassiactivate kbo, not lpo
2009-07-09 Claudio Sacerdoti... ...
2009-07-09 Claudio Sacerdoti... Bug fixed (non-captured variable).
2009-07-08 Claudio Sacerdoti... eq moved to CProp
next