]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
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...
2009-04-17 Claudio Sacerdoti... Some improvements.
2009-04-17 Claudio Sacerdoti... ...
2009-04-16 Ferruccio GuidiProcedural: we corrected two errors about the handling...
2009-04-16 Claudio Sacerdoti... Bug: let-ins are always automatically folded!
2009-04-16 Claudio Sacerdoti... ...
2009-04-16 Claudio Sacerdoti... test/a.ma => tests/ng_tactics.ma, with nassert here...
2009-04-16 Claudio Sacerdoti... Replaced long, bugged implementation of letin-tac with...
2009-04-16 Claudio Sacerdoti... Added ppterm.
2009-04-16 Claudio Sacerdoti... The context is now parsed in the reverse (right) order.
2009-04-16 Claudio Sacerdoti... ...
2009-04-16 Enrico TassiUniverse is used only locally to tactics/
2009-04-16 Enrico Tassiadded an exception
2009-04-15 Ferruccio Guidi- transcript: bugfix
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete
2009-04-14 Claudio Sacerdoti... Trick: the refiner always subst-expands the outtype...
2009-04-14 Claudio Sacerdoti... Bug fixed in two lines + 5 lines of comment.
2009-04-14 Claudio Sacerdoti... assert_tac now takes a list of sequents and also checks...
2009-04-14 Claudio Sacerdoti... New debugging tactic nassert:
2009-04-12 Claudio Sacerdoti... Semantic selection back again (but no semantic cut...
2009-04-12 Claudio Sacerdoti... Match is now rendered as best as possible.
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render...
2009-04-09 Ferruccio Guidi- character: we adjusted some "autobatch" parameters
2009-04-09 Claudio Sacerdoti... The substitution is now taken in account when printing...
2009-04-09 Enrico Tassiadded letin, still broken
2009-04-09 Enrico Tassi...
2009-04-09 Enrico Tassinew tactic whd implemented
2009-04-09 Enrico Tassi- change implemented in 4 lines
2009-04-09 Enrico Tassi- generalize finished
2009-04-09 Enrico Tassi?_OS1 := C[ ?_IN ]
2009-04-09 Enrico Tassifixed modules order
2009-04-09 Enrico Tassiminor fixes
2009-04-09 Enrico Tassi...
2009-04-09 Claudio Sacerdoti... ...
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very...
2009-04-08 Claudio Sacerdoti... Just to make it compile again.
2009-04-08 Enrico Tassigeneralized is half-implemented (still broken)
2009-04-08 Enrico TassiAnalizyng the inductive type of the eliminated term and
2009-04-07 Claudio Sacerdoti... - nrewrite ((very?) rough implementation)
2009-04-07 Claudio Sacerdoti... - more progress towards generalize, but I am stuck now
2009-04-07 Enrico Tassi- select_tac honors the hypotheses pattern when require...
2009-04-07 Enrico Tassiselect honors the substitution
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and...
2009-04-06 Claudio Sacerdoti... ...
2009-04-06 Enrico Tassitactic cases works! delift clears tags
2009-04-06 Enrico Tassieta-contraction was made on the wrong term
2009-04-06 Enrico Tassiunification:
next