]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2009-05-17 Claudio Sacerdoti... maxmeta function to return the heighest meta used so far
2009-05-17 Claudio Sacerdoti... alpha_eq exported
2009-05-17 Claudio Sacerdoti... alpha_eq defined and exported
2009-05-17 Claudio Sacerdoti... efficiency improvement (buffers are now used everywhere)
2009-05-17 Claudio Sacerdoti... ...
2009-05-17 Enrico Tassibyte tests disabled
2009-05-15 Enrico Tassiadded patch to not unify any term containing the in_sco...
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth...
2009-05-15 Claudio Sacerdoti... Cosmetic.
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
2009-05-14 Ferruccio Guidi- libraryObjects: new default "natural numbers" with...
2009-05-13 Ferruccio Guidiinterpretations placed right after the corresponding...
2009-05-13 Ferruccio Guidi- matitaEngine: some commands like "coercion" must...
2009-05-13 Andrea AspertiThe singature of the "by" universe is added to the...
2009-05-13 Andrea AspertiVia un'altra linea...
2009-05-13 Andrea AspertiSempre piu' breve
2009-05-13 Andrea AspertiSignature is computed on the initial goal, once and...
2009-05-12 Claudio Sacerdoti... Do we really want to generate eliminators for nested...
2009-05-12 Claudio Sacerdoti... All weakly positive types but imbricated ones are now...
2009-05-12 Ferruccio Guidi- Procedural: we now reconstruct "let H := v in t"...
2009-05-12 Andrea AspertiWe only filter the smart candidates w.r.t the signature
2009-05-11 Claudio Sacerdoti... Some experiments in generation of elimination principles.
2009-05-11 Claudio Sacerdoti... ppsubst commented out in ppobj
2009-05-11 Claudio Sacerdoti... Bug fixed: the relevance list can be shorted then leftn...
2009-05-11 Claudio Sacerdoti... Missing spaces inserted here and there.
2009-05-11 Claudio Sacerdoti... - non_punctuational_tacticals ported to NG
2009-05-11 Claudio Sacerdoti... Buffers are now used everywhere for speed-up.
2009-05-11 Claudio Sacerdoti... New function list_iter_sep.
2009-05-11 Andrea AspertiA few lemmas about inclusion.
2009-05-11 Andrea AspertiMore automation
2009-05-10 Claudio Sacerdoti... - critical bug fixed in NCicSubstitution.lift:
2009-05-08 Claudio Sacerdoti... Stupid typing error fixed.
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Claudio Sacerdoti... Bug fixed: left parameters of constructors were unified...
2009-05-08 Claudio Sacerdoti... Bug fixed: refinement of mutual recursive definitions...
2009-05-08 Claudio Sacerdoti... Improved tests (for left parameters and mutual recursiv...
2009-05-08 Claudio Sacerdoti... Bug fixed in refinement of inductive types: left parame...
2009-05-08 Claudio Sacerdoti... 1) better implementation of NObj that now calls recursi...
2009-05-08 Claudio Sacerdoti... The relevance list can be shorter than leftno (when...
2009-05-08 Claudio Sacerdoti... Bug fixed in interpretation of records (the type was...
2009-05-08 Andrea AspertiConstructors are closed with thier types when computing...
2009-05-08 Andrea Aspertiversione automatizzata
2009-05-08 Andrea Aspertisymmetry of inequality sym_neq
2009-05-07 Ferruccio Guididocumentation for the inline command
2009-05-06 Ferruccio Guidi- dependenciesParser: updated to new inline syntax
2009-05-06 Ferruccio GuidiLAMBDA-TYPES: mma's recommitted because inline syntax...
2009-05-06 Ferruccio Guidi- cicUtil: is_sober now detects folded applications
2009-05-06 Enrico Tassiapply and auto.equational_case call saturation.solve_na...
2009-05-06 Enrico Tassiupdated comment
2009-05-05 Ferruccio Guidi- Procedural: new flag "level=n" to control the reconst...
2009-05-05 Ferruccio Guidi- hExtlib: new function "list_assoc_all"
2009-05-05 Enrico Tassi- pretty printer made robust in face of list_nth
2009-05-05 Enrico Tassimore tests
2009-05-05 Andrea AspertiNuova gestione di "by" per auto.
2009-05-05 Andrea Aspertiautobatch by
2009-05-01 Ferruccio Guidi- librarian: 3 bugs fixed in the building system:
2009-04-30 Enrico Tassirun check_if_goal_is_solved on all goals (active+passive)
2009-04-30 Matthias PuechAdded an option --enable-annot to the configure to...
2009-04-30 Andrea AspertiMinor changes pro-automation
2009-04-30 Andrea AspertiAdded a passive table
2009-04-30 Andrea AspertiCalling paramodulation instead of demod_all
2009-04-29 Claudio Sacerdoti... Refinement of inductive type implemented.
2009-04-29 Ferruccio Guidi- procedural: bugfix in "Barendregt convention" test
2009-04-29 Enrico Tassi...
2009-04-29 Enrico Tassicall paramod instead of solve_Rewrite
2009-04-29 Enrico Tassino typing
2009-04-29 Enrico Tassimany checks guarded with if Utils.debug_metas
2009-04-29 Claudio Sacerdoti... Records are now interpreted in the NG (but I am sure...
2009-04-28 Claudio Sacerdoti... Inductive definitions are now interpreted (but records...
2009-04-28 Claudio Sacerdoti... Last commit by Ferruccio reverted since it breaks the...
2009-04-28 Ferruccio GuidicicNotationUtil: in fresh_name_generator, "\eta" replac...
2009-04-28 Enrico Tassidepenalization of smart apply inside auto, that is...
2009-04-28 Enrico Tassifixed bug, demodulation was keeping results not strictl...
2009-04-28 Enrico Tassihuge commit in automation:
2009-04-27 Ferruccio GuidimatitacLib: bugfix in .moo generation
2009-04-26 Claudio Sacerdoti... The backward compatible management of aliases for NG...
2009-04-25 Claudio Sacerdoti... It is now possible for commands processed by grafiteEng...
2009-04-25 Claudio Sacerdoti... Lookup_in_library implemented for new objects. Basicall...
2009-04-25 Claudio Sacerdoti... It is now possible to declare new aliases using the...
2009-04-25 Ferruccio Guidi- matitacLib: lexicon status and grafite status where...
2009-04-25 Claudio Sacerdoti... The translation from old aliases to new references...
2009-04-25 Claudio Sacerdoti... Apply subst implemented also for Fixpoints.
2009-04-25 Claudio Sacerdoti... Type for list_index improved.
2009-04-25 Claudio Sacerdoti... Slightly improved type for list_index.
2009-04-25 Claudio Sacerdoti... New utility function list_index (useful in many places...
2009-04-25 Claudio Sacerdoti... Better error message.
2009-04-25 Claudio Sacerdoti... Debug option reverted.
2009-04-25 Ferruccio Guidi- matitacLib: better handling of the callbacks for...
2009-04-24 Claudio Sacerdoti... - Grammar for all obj commands ported to NG (let recs...
2009-04-24 Claudio Sacerdoti... Quick&dirty implementation of neqd:
2009-04-22 Ferruccio Guidi- transcript: we have now two styles of mma's from...
2009-04-22 Wilmer Ricciottisyntax colouring for inverters
2009-04-22 Wilmer RicciottiDisabled debug prints in the inversion principle.
2009-04-22 Wilmer RicciottiNew command "inverter" used to generate an induction...
2009-04-22 Enrico Tassidemodulate takes an extra argument 'all', if present...
2009-04-21 Ferruccio Guidi- MatitaMisc: we factorized here the function out_pream...
2009-04-21 Enrico Tassifixed last file restricting auto tables
2009-04-20 Enrico Tassi- init_cache_and_tables rewritten using the automation_...
2009-04-20 Claudio Sacerdoti... Bug fixed: variable capture in previous commit prevente...
next