]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2008-06-06 Andrea Asperticleanup
2008-06-06 Andrea AspertiCleanup.
2008-06-06 Claudio Sacerdoti... sieve.ma now depends only on primes.ma
2008-06-06 Andrea AspertiAdded frac.ma
2008-06-06 Andrea AspertiAdded Qplus_andrea.ma
2008-06-06 Claudio Sacerdoti... Reduce reduction tactic got rid of a long time ago.
2008-06-05 Claudio Sacerdoti... Eratosthene's sieve factorized out of nat/bertrand...
2008-06-05 Enrico Tassi....
2008-06-05 Enrico Tassiadded order_continuity
2008-06-05 Enrico Tassisandwich is back
2008-06-04 Wilmer RicciottiProof-irrelevance check for all applications (first...
2008-06-04 Wilmer Ricciottiincomplete irrelevance test commented out
2008-06-03 Claudio Sacerdoti... Some proofs on enumerator and denominator.
2008-06-03 Claudio Sacerdoti... More work on rational numbers with unique representations.
2008-06-03 Enrico Tassisome work on uniformity
2008-06-03 Enrico Tassiend of section 2.2
2008-06-03 Enrico Tassiproof refactored
2008-06-03 Enrico Tassixxx
2008-06-01 Enrico Tassimore work on supremum
2008-05-30 Enrico TassiCProp hierarchy is there!
2008-05-30 Enrico Tassiirrelevance check half implemented but already impossib...
2008-05-30 Enrico Tassi...
2008-05-30 Enrico Tassigarbage removed
2008-05-30 Enrico Tassimore work on dama
2008-05-30 Enrico Tassiprod moved under lambda-prolog unification case
2008-05-30 Enrico Tassiadded CProp
2008-05-30 Enrico Tassithanks to the fact that we convert well typed term...
2008-05-30 Enrico Tassiadded a bit more reduction in case Prod v.s. term,...
2008-05-29 Enrico Tassirelevance check partially implemented but bugged since...
2008-05-29 Enrico Tassicase not unfilding fixed
2008-05-29 Enrico TassiCProp, since it was defined in CoRN as a Type, is predi...
2008-05-29 Enrico Tassi0.5.1 released
2008-05-29 Enrico Tassiunused variables removed
2008-05-29 Enrico Tassiref sync check fixed controlling fix/cofix coherence
2008-05-29 Enrico Tassi...
2008-05-29 Enrico Tassifirst page of the new dama proof
2008-05-29 Enrico Tassi...
2008-05-29 Enrico Tassithe type of the match was obtained reducing the outtype
2008-05-28 Enrico Tassi...
2008-05-28 Enrico Tassidama restarted
2008-05-28 Enrico Tassicleanup
2008-05-28 Enrico Tassithe attempt of completing dama using duality frozen
2008-05-28 Enrico Tassi0.5.1
2008-05-27 Enrico Tassi...
2008-05-27 Enrico Tassismarter lexer needed by lambda-delta that is splitting...
2008-05-27 Enrico Tassi...
2008-05-27 Enrico TassiCoRN moved in contribs
2008-05-27 Enrico Tassifrst step to move away the CoRN stuff
2008-05-27 Enrico Tassifrst step to move away the CoRN stuff
2008-05-27 Enrico Tassiauto calls cleanup\
2008-05-26 Enrico Tassibetter description of declarative tactics
2008-05-26 Enrico Tassinew, more rigid syntax, for auto_params affecting the...
2008-05-26 Enrico TassiUniverse.key was not used to index terms, but was used...
2008-05-26 Ferruccio Guidibetter presentation of lambda-delta
2008-05-26 Ferruccio Guidi- some bugs fixed in the domain-based preorders on...
2008-05-26 Enrico Tassiadded comment for zack
2008-05-26 Enrico Tassi...
2008-05-26 Enrico Tassiauto syntax updated
2008-05-26 Enrico Tassi...
2008-05-24 Enrico Tassi...
2008-05-24 Enrico Tassiorder of goals changes, open ones are preferred to...
2008-05-21 Enrico Tassiminimal implementation of left parameters display
2008-05-21 Enrico Tassi0.5.1 should be realased soon, the bug that was affecti...
2008-05-19 Claudio Sacerdoti... Here is where we should add relevance checks.
2008-05-19 Claudio Sacerdoti... Bug fixed in computation of leftnos: variables were...
2008-05-19 Claudio Sacerdoti... Code simplification.
2008-05-19 Claudio Sacerdoti... Added cprop <= type constraint.
2008-05-19 Claudio Sacerdoti... We do not need to give cprop a special status yet.
2008-05-19 Claudio Sacerdoti... ...
2008-05-19 Claudio Sacerdoti... CProp dropped in favour of a cprop universe exported...
2008-05-19 Enrico Tassiadded leftno to references f inductive types and constr...
2008-05-19 Enrico Tassiadded aps generation
2008-05-19 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-19 Enrico Tassi...
2008-05-19 Enrico Tassirenamed add_le_constraint to add_constraint since it...
2008-05-18 Claudio Sacerdoti... ...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassirun fsub during night
2008-05-18 Claudio Sacerdoti... Bug fixed: when computing the left arguments, I was...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassinames fixed accoding to the new ones generated after...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassirevert last commit, context' -> context (added comment)
2008-05-18 Enrico Tassiusing the right names in the context to check match...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... New missing check implemented: the left parameters...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent products in inductive types arities...
2008-05-18 Claudio Sacerdoti... This commit avoids cleaning dummy dependent types in...
2008-05-18 Claudio Sacerdoti... Implemented translation of inductive types from the...
2008-05-18 Claudio Sacerdoti... Serious bug fixed: the max of two universes was compute...
2008-05-18 Claudio Sacerdoti... Synch with the paper.
next