]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics
New argument (the identifier) to generalize.
[helm.git] / helm / ocaml / tactics /
2005-06-27 Enrico Tassisupport for _ in binders, and a more coplex pattern...
2005-06-27 Claudio Sacerdoti... * auto_tac removed (it can be found in CVS)
2005-06-27 Enrico Tassi1) moved select and pattern_of from cicUtil to proofEng...
2005-06-27 Enrico Tassifixed LApply pretty printing
2005-06-25 Ferruccio Guidifirst working (?) version of lapply
2005-06-25 Ferruccio Guidifirs wrking (?) version of lapply
2005-06-24 Ferruccio Guidilapply tactic continued
2005-06-24 Enrico Tassinew implementation (due to paths).
2005-06-24 Enrico Tassistupid rename
2005-06-24 Enrico Tassinow we use rplace_lifting_csc since the what must NOT...
2005-06-24 Claudio Sacerdoti... New implementation of experimental_hint/auto (called...
2005-06-24 Claudio Sacerdoti... New functions UriManager.uri_is_var, UriManager.uri_is_con.
2005-06-24 Claudio Sacerdoti... Asts generalized: a lot of tactics where restricted...
2005-06-23 Enrico TassiMuch simpler (and slightly more performant) implementat...
2005-06-23 Claudio Sacerdoti... Tactic generalize ported to patterns and activated...
2005-06-17 Enrico Tassiadded support for goal patterns
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri
2005-06-17 Claudio Sacerdoti... many strings that are supposed to be URIs are now UriMa...
2005-06-16 Claudio Sacerdoti... Locally implemented print_context replaced by CicPp...
2005-06-16 Andrea AspertiA cleaned version of auto_tac_new.
2005-06-16 Stefano Zacchiroliadded depth and width (optional) parameters to auto_tac_new
2005-06-15 Ferruccio Guidibeginning of the tactics lapply and fwd
2005-06-15 Enrico Tassiapply_tac used to calculate the type of the term before...
2005-06-10 Claudio Sacerdoti... Got rid of a few warnings.
2005-06-10 Claudio Sacerdoti... an assert failure changed to an exception and a bit...
2005-06-01 Enrico Tassipaths trough terms implemented with a nice hack :)
2005-06-01 Enrico Tassiremoved debug prerr_endline
2005-05-31 Enrico Tassi added comment
2005-05-31 Enrico Tassiimplemented normalize (used in new_metasenv_for_apply)
2005-05-31 Enrico Tassifix
2005-05-30 Andrea Aspertiadded intros n
2005-05-27 Enrico Tassiremoved debug prerr_endline
2005-05-25 Enrico Tassiapply now tries both to reduce and to not reduce the...
2005-05-24 Enrico Tassireverted to ==
2005-05-24 Enrico Tassinew simpl semantic (now = and not == since you can...
2005-05-24 Enrico Tassiadded lost elim_intros_tac
2005-05-24 Andrea AspertiAdded a new tactic elim_intros (without simpl of the...
2005-05-20 Andrea AspertiAdded a whd on ty in new_metasenv for apply, in order...
2005-05-20 Andrea AspertiHint repaired (an erroneous commit by myself).
2005-05-19 Stefano Zacchirolicommented out some debugging messages
2005-05-17 Enrico Tassiaded comment
2005-05-17 Stefano Zacchirolibugfix in elim, cardinality constraint should >= 1...
2005-05-16 Enrico Tassifixed instance
2005-05-13 Alberto Griggioexported new_metasenv_for_apply, needed by the paramodu...
2005-05-06 Enrico Tassifactorization of rewrite.
2005-05-05 Andrea AspertiSome modifications due to instance.
2005-05-03 Enrico Tassiadded sqlStatements module (contains all CREATE TABLE...
2005-05-03 Enrico Tassifix for instance
2005-05-03 Andrea AspertiFirst version of instance.
2005-05-02 Enrico Tassiattached auto
2005-04-29 Enrico Tassimain constants set is closed with constants types
2005-04-29 Stefano Zacchiroliadded rating parameter to at_least (used by elim)
2005-04-27 Stefano Zacchirolimerged changes from the svn fork by me and Enrico
2005-04-22 Stefano Zacchiroliremoved debugging print
2005-04-22 Stefano Zacchiroliuses new at_least with criteria on constants number...
2005-03-22 Claudio Sacerdoti... Bug fixed in assumption_tac: a missing (lift n) when...
2005-03-15 Stefano Zacchiroli- handle metavariables: if at least one of them is...
2005-02-04 Enrico Tassilocate now searched bot the standard library and the...
2005-02-04 Stefano Zacchiroli- removed dependency on mathql
2005-02-03 Enrico Tassinew metadataTypes interface (with ownerize function)
2005-02-01 Enrico Tassireverder change. no more owner passed to the locate.
2005-02-01 Enrico Tassiadded owner support to the disambiguator (now locate...
2005-01-21 Stefano Zacchiroli- attributes support
2005-01-17 Enrico Tassinew cicEnvironment implementation
2004-12-06 Andrea AspertiNew version of auto with "width".
2004-12-03 Stefano Zacchirolichanged "locate" so that it supports shell-like pattern...
2004-12-02 Stefano Zacchiroli*** empty log message ***
2004-12-01 Enrico TassiAdded universes handling. The PRE_UNIVERSES tag may...
2004-11-30 Andrea AspertiBug in the management of substitutions into auto corrected.
2004-11-29 Stefano Zacchirolipasses ~subst to FreshNameGenerator
2004-11-05 Stefano Zacchiroli- added Tactics module as a common point where tactics...
2004-11-04 Andrea AspertiAuto moved to a new file autoTactic.ml
2004-11-04 Andrea AspertiNew version(s) of hint. One more stable (hint) and...
2004-11-03 Stefano Zacchirolino longer use Dbi module but directly use Mysql module...
2004-10-25 Stefano Zacchirolisort hint's result accordingly to the "least goal left...
2004-10-25 Stefano Zacchiroli- added var selection boolean to locate
2004-10-25 Stefano Zacchiroliadded vars selection boolean on locate
2004-10-22 Andrea Aspertiimplemented elim query
2004-10-22 Andrea Aspertibugfix: handle overflow in powerset cardinality
2004-10-22 Stefano Zacchiroli- reimplemented tacticChaser and friends in term of...
2004-10-22 Andrea Asperti- added (hack) apply_tac_verbose (for auto)
2004-10-22 Andrea Aspertiported to typed explicit subst
2004-10-21 Stefano Zacchiroliadded reference to MetadataQuery (now it builds properly)
2004-10-21 Stefano Zacchiroliimplemented in place old Filter_auto filtering
2004-10-21 Stefano Zacchirolifixed a buggy pattern matching
2004-10-20 Stefano Zacchirolitop level query module
2004-10-12 Stefano Zacchirolisetting goal doesn't change history status
2004-10-04 Stefano Zacchirolisplitted History module out of StatefulProofEngine
2004-10-04 Stefano Zacchiroli- splitted out History module
2004-09-20 Stefano Zacchiroliadded initial_status
2004-09-01 Andrea AspertiBug fixing: the call to MQueryMisc.wrong_xpointer_forma...
2004-07-13 Matteo SelmiModified filtering function
2004-07-05 Stefano Zacchirolicommented out some debugging instructions
2004-07-02 Claudio Sacerdoti... Bug fixed: eta_expand did not perform any recursion...
2004-07-01 Stefano ZacchiroliNew handling of substitution:
2004-06-28 Andrea Aspertifixed typo
2004-06-18 Matteo SelmiCorrections to "auto" tactic
2004-06-18 Claudio Sacerdoti... elim_tac rewritten almost entirely. It is now based...
2004-06-18 Claudio Sacerdoti... Added new function compare_metasenvs.
2004-06-18 Claudio Sacerdoti... Comments changed.
next