]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics
dependencies between statuses simplified
[helm.git] / helm / software / components / tactics /
2010-03-31 Andrea AspertiTracing mechanism for auto. Interface changed to solve...
2010-03-24 Claudio Sacerdoti... ...
2009-11-16 Wilmer RicciottiImplementation of ndestruct tactic (including destructi...
2009-10-06 Wilmer RicciottiInverters/Inversion:
2009-10-05 Enrico Tassiadded auto_cache in the dupable status after an
2009-10-02 Wilmer RicciottiUpdated command ninverter. Syntax:
2009-10-02 Claudio Sacerdoti... ...
2009-09-30 Wilmer RicciottiAdded initial support for inversion principles in Matit...
2009-09-09 Enrico Tassidepends
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-06-25 Ferruccio Guidi- some depend files :)
2009-06-25 Enrico Tassiinitial import of standalone matitaprover binary
2009-06-15 Enrico Tassihuge commit regarding the grafite_status:
2009-06-10 Ferruccio Guidi- library/list/list.ma: unused code commented
2009-06-03 Claudio Sacerdoti... Huge commit with several changes:
2009-05-27 Andrea AspertiAvoiding to filter the application of congruence equations
2009-05-25 Enrico Tassinasty change in the lexer/parser:
2009-05-22 Andrea AspertiPruning candidates in the applicative case for equalities.
2009-05-20 Andrea AspertiRemoved a silly type check
2009-05-18 Enrico Tassinothing special
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth...
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
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 AspertiSignature is computed on the initial goal, once and...
2009-05-12 Andrea AspertiWe only filter the smart candidates w.r.t the signature
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Andrea AspertiConstructors are closed with thier types when computing...
2009-05-06 Enrico Tassiapply and auto.equational_case call saturation.solve_na...
2009-05-05 Andrea AspertiNuova gestione di "by" per auto.
2009-04-30 Enrico Tassirun check_if_goal_is_solved on all goals (active+passive)
2009-04-30 Andrea AspertiAdded a passive table
2009-04-30 Andrea AspertiCalling paramodulation instead of demod_all
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-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-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 Enrico Tassifixed last file restricting auto tables
2009-04-20 Enrico Tassi- init_cache_and_tables rewritten using the automation_...
2009-04-16 Enrico TassiUniverse is used only locally to tactics/
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete
2009-03-25 Enrico Tassinew tactics are almost ready
2009-03-16 Andrea AspertiNew parameters for applyS: 10 20.
2009-03-10 Andrea AspertiA version of applyS with bounded iterations of given_cl...
2009-03-10 Andrea AspertiRemoved the context from the metasenv to avoid trivial...
2009-02-15 Enrico Tassicommented some printings
2009-02-12 Andrea Aspertierrata corrige.
2009-02-12 Andrea AspertiFixed a problem of lifting.
2009-02-03 Enrico Tassicase tactic first tries with a simple outtype and then...
2009-01-15 Enrico Tassi- name mangling changed, added __ to separate additiona...
2009-01-13 Enrico Tassimany changes regarding coercions:
2009-01-08 Enrico Tassimore composites to make all happy!
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator
2008-11-16 Enrico Tassiremoved some printings
2008-11-16 Enrico Tassiremoved some printings
2008-11-07 Andrea Aspertidebug=false
2008-11-07 Andrea AspertiSignature_of has been closed with respect to constructors.
2008-11-07 Andrea AspertiThe signature in "retrieve equations" must be extended...
2008-11-06 Enrico Tassithe passive set and passive list are expected to have...
2008-11-05 Enrico Tassinew internal flags for auto:
2008-11-05 Enrico Tassiduplicate entry in menv avoided
2008-11-04 Andrea AspertiCalling unification instead of matching when checking...
2008-11-03 Enrico Tassiremoved prerr_endline
2008-11-03 Enrico Tassidebug=false
2008-11-01 Enrico Tassiadded lazy
2008-10-29 Andrea AspertiPropagation of changes in paramodulation.
2008-10-29 Andrea AspertiExported a couple of functions.
2008-10-29 Andrea AspertiAdded a in_universe function
2008-10-29 Andrea Aspertipropagation of changes in other paramodulation files.
2008-10-29 Andrea AspertiNew demod function working for arbitary goals.
2008-10-29 Andrea AspertiEnforcing the disjoint invariant between metasenvs.
2008-10-29 Andrea AspertiMain change: added a parameter to build_equality_proof...
2008-09-26 Enrico Tassiauto was compiraing lazy proof terms with = ... fixed
2008-09-26 Enrico Tassilazy proof term to increase sharing and decrease memory...
2008-09-19 Enrico Tassimore abstract discrimination tree
2008-09-19 Enrico Tassibetter abstraction to allow 1 discrimination tree imple...
2008-09-19 Enrico TassiRevised discrimination tree implementation:
2008-09-19 Andrea AspertiA temporary patch to demodulation theorem.
2008-09-09 Enrico Tassisome work to make tries "printable", fixed comparison...
2008-08-28 Ferruccio GuidicicDischarge: new module for discharging the explicit...
2008-07-07 Enrico Tassisimplified coercDb implementation with additional info...
2008-07-04 Ferruccio Guidi- Procedural: bug fix in rendering the application...
2008-07-02 Ferruccio Guidi- new tactic applyP for use in the *P*rocedural script...
2008-07-02 Enrico Tassicalculation of the sort user to choose the rewriting...
2008-06-19 Claudio Sacerdoti... 1. bug fixed in generalize_pattern: a lazy const_tac...
2008-06-08 Claudio Sacerdoti... Bug fixed: wrong default pattern for generalize.
2008-06-08 Claudio Sacerdoti... Hypotheses patterns for elim implemented. No more need...
2008-05-30 Enrico TassiCProp hierarchy is there!
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-24 Enrico Tassiorder of goals changes, open ones are preferred to...
2008-04-22 Enrico Tassioblivion ugraph everywhere outside the kernel
2008-04-01 Enrico Tassibetter check for progress
2008-04-01 Enrico Tassiprogress made better, still not perfect
next