]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
All the tactics have been ported to use the objects in LibraryObjects.
[helm.git] / helm / ocaml / tactics /
2005-07-04 Claudio Sacerdoti... All the tactics have been ported to use the objects... tree | commitdiff
2005-07-04 Claudio Sacerdoti... Comestic changes. tree | commitdiff
2005-07-04 Claudio Sacerdoti... Cosmetic changes. tree | commitdiff
2005-07-02 Claudio Sacerdoti... All the equalityTactics have now been ported to use... tree | commitdiff
2005-07-01 Claudio Sacerdoti... replace tactic reimplemented. tree | commitdiff
2005-07-01 Claudio Sacerdoti... pattern_of function reimplemented. Now it takes a term... tree | commitdiff
2005-07-01 Claudio Sacerdoti... The replace tactic is now working again. It can now... tree | commitdiff
2005-07-01 Claudio Sacerdoti... Signature of fwdSimpl changed to get rid of a warning. tree | commitdiff
2005-07-01 Claudio Sacerdoti... 1. change_tac moved from PrimitiveTactics to ReductionT... tree | commitdiff
2005-06-30 Claudio Sacerdoti... Signature and concrete syntax of fold fixed. tree | commitdiff
2005-06-30 Ferruccio Guidilapply and fwd improved tree | commitdiff
2005-06-30 Claudio Sacerdoti... The rewrite_* set of tactics is now working again.... tree | commitdiff
2005-06-30 Claudio Sacerdoti... Bug fixed: a wrong lift made select unuseful when wante... tree | commitdiff
2005-06-30 Claudio Sacerdoti... 1. rewrite_* and rewrite_back_* merged into one function tree | commitdiff
2005-06-30 Claudio Sacerdoti... Oooops. I forgot the convertibility test that makes... tree | commitdiff
2005-06-30 Claudio Sacerdoti... The tactic change is now working again. Moreover, it... tree | commitdiff
2005-06-30 Claudio Sacerdoti... A bit of renaming in the code to make it more clear. tree | commitdiff
2005-06-30 Claudio Sacerdoti... Obsolete comment removed. tree | commitdiff
2005-06-30 Claudio Sacerdoti... Stupid bug fixed (a completely erroneous assert false... tree | commitdiff
2005-06-30 Claudio Sacerdoti... This commit makes ProofEngineHelpers.select reach its... tree | commitdiff
2005-06-29 Claudio Sacerdoti... 1. new syntax for patterns: tree | commitdiff
2005-06-29 Enrico Tassiremoved profiling function (now a stub is used instead) tree | commitdiff
2005-06-29 Claudio Sacerdoti... Incredible bug of simpl fixed: the stack (in the termin... tree | commitdiff
2005-06-29 Ferruccio Guidilapply reimplemented using letin_tac tree | commitdiff
2005-06-28 Ferruccio Guidilapply improved tree | commitdiff
2005-06-27 Claudio Sacerdoti... 1. interface of replace generalized to patterns tree | commitdiff
2005-06-27 Claudio Sacerdoti... A few other tactics made available to matita. tree | commitdiff
2005-06-27 Enrico Tassisupport for _ in binders, and a more coplex pattern... tree | commitdiff
2005-06-27 Claudio Sacerdoti... * auto_tac removed (it can be found in CVS) tree | commitdiff
2005-06-27 Enrico Tassi1) moved select and pattern_of from cicUtil to proofEng... tree | commitdiff
2005-06-27 Enrico Tassifixed LApply pretty printing tree | commitdiff
2005-06-25 Ferruccio Guidifirst working (?) version of lapply tree | commitdiff
2005-06-25 Ferruccio Guidifirs wrking (?) version of lapply tree | commitdiff
2005-06-24 Ferruccio Guidilapply tactic continued tree | commitdiff
2005-06-24 Enrico Tassinew implementation (due to paths). tree | commitdiff
2005-06-24 Enrico Tassistupid rename tree | commitdiff
2005-06-24 Enrico Tassinow we use rplace_lifting_csc since the what must NOT... tree | commitdiff
2005-06-24 Claudio Sacerdoti... New implementation of experimental_hint/auto (called... tree | commitdiff
2005-06-24 Claudio Sacerdoti... New functions UriManager.uri_is_var, UriManager.uri_is_con. tree | commitdiff
2005-06-24 Claudio Sacerdoti... Asts generalized: a lot of tactics where restricted... tree | commitdiff
2005-06-23 Enrico TassiMuch simpler (and slightly more performant) implementat... tree | commitdiff
2005-06-23 Claudio Sacerdoti... Tactic generalize ported to patterns and activated... tree | commitdiff
2005-06-17 Enrico Tassiadded support for goal patterns tree | commitdiff
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri tree | commitdiff
2005-06-17 Claudio Sacerdoti... many strings that are supposed to be URIs are now UriMa... tree | commitdiff
2005-06-16 Claudio Sacerdoti... Locally implemented print_context replaced by CicPp... tree | commitdiff
2005-06-16 Andrea AspertiA cleaned version of auto_tac_new. tree | commitdiff
2005-06-16 Stefano Zacchiroliadded depth and width (optional) parameters to auto_tac_new tree | commitdiff
2005-06-15 Ferruccio Guidibeginning of the tactics lapply and fwd tree | commitdiff
2005-06-15 Enrico Tassiapply_tac used to calculate the type of the term before... tree | commitdiff
2005-06-10 Claudio Sacerdoti... Got rid of a few warnings. tree | commitdiff
2005-06-10 Claudio Sacerdoti... an assert failure changed to an exception and a bit... tree | commitdiff
2005-06-01 Enrico Tassipaths trough terms implemented with a nice hack :) tree | commitdiff
2005-06-01 Enrico Tassiremoved debug prerr_endline tree | commitdiff
2005-05-31 Enrico Tassi added comment tree | commitdiff
2005-05-31 Enrico Tassiimplemented normalize (used in new_metasenv_for_apply) tree | commitdiff
2005-05-31 Enrico Tassifix tree | commitdiff
2005-05-30 Andrea Aspertiadded intros n tree | commitdiff
2005-05-27 Enrico Tassiremoved debug prerr_endline tree | commitdiff
2005-05-25 Enrico Tassiapply now tries both to reduce and to not reduce the... tree | commitdiff
2005-05-24 Enrico Tassireverted to == tree | commitdiff
2005-05-24 Enrico Tassinew simpl semantic (now = and not == since you can... tree | commitdiff
2005-05-24 Enrico Tassiadded lost elim_intros_tac tree | commitdiff
2005-05-24 Andrea AspertiAdded a new tactic elim_intros (without simpl of the... tree | commitdiff
2005-05-20 Andrea AspertiAdded a whd on ty in new_metasenv for apply, in order... tree | commitdiff
2005-05-20 Andrea AspertiHint repaired (an erroneous commit by myself). tree | commitdiff
2005-05-19 Stefano Zacchirolicommented out some debugging messages tree | commitdiff
2005-05-17 Enrico Tassiaded comment tree | commitdiff
2005-05-17 Stefano Zacchirolibugfix in elim, cardinality constraint should >= 1... tree | commitdiff
2005-05-16 Enrico Tassifixed instance tree | commitdiff
2005-05-13 Alberto Griggioexported new_metasenv_for_apply, needed by the paramodu... tree | commitdiff
2005-05-06 Enrico Tassifactorization of rewrite. tree | commitdiff
2005-05-05 Andrea AspertiSome modifications due to instance. tree | commitdiff
2005-05-03 Enrico Tassiadded sqlStatements module (contains all CREATE TABLE... tree | commitdiff
2005-05-03 Enrico Tassifix for instance tree | commitdiff
2005-05-03 Andrea AspertiFirst version of instance. tree | commitdiff
2005-05-02 Enrico Tassiattached auto tree | commitdiff
2005-04-29 Enrico Tassimain constants set is closed with constants types tree | commitdiff
2005-04-29 Stefano Zacchiroliadded rating parameter to at_least (used by elim) tree | commitdiff
2005-04-27 Stefano Zacchirolimerged changes from the svn fork by me and Enrico tree | commitdiff
2005-04-22 Stefano Zacchiroliremoved debugging print tree | commitdiff
2005-04-22 Stefano Zacchiroliuses new at_least with criteria on constants number... tree | commitdiff
2005-03-22 Claudio Sacerdoti... Bug fixed in assumption_tac: a missing (lift n) when... tree | commitdiff
2005-03-15 Stefano Zacchiroli- handle metavariables: if at least one of them is... tree | commitdiff
2005-02-04 Enrico Tassilocate now searched bot the standard library and the... tree | commitdiff
2005-02-04 Stefano Zacchiroli- removed dependency on mathql tree | commitdiff
2005-02-03 Enrico Tassinew metadataTypes interface (with ownerize function) tree | commitdiff
2005-02-01 Enrico Tassireverder change. no more owner passed to the locate. tree | commitdiff
2005-02-01 Enrico Tassiadded owner support to the disambiguator (now locate... tree | commitdiff
2005-01-21 Stefano Zacchiroli- attributes support tree | commitdiff
2005-01-17 Enrico Tassinew cicEnvironment implementation tree | commitdiff
2004-12-06 Andrea AspertiNew version of auto with "width". tree | commitdiff
2004-12-03 Stefano Zacchirolichanged "locate" so that it supports shell-like pattern... tree | commitdiff
2004-12-02 Stefano Zacchiroli*** empty log message *** tree | commitdiff
2004-12-01 Enrico TassiAdded universes handling. The PRE_UNIVERSES tag may... tree | commitdiff
2004-11-30 Andrea AspertiBug in the management of substitutions into auto corrected. tree | commitdiff
2004-11-29 Stefano Zacchirolipasses ~subst to FreshNameGenerator tree | commitdiff
2004-11-05 Stefano Zacchiroli- added Tactics module as a common point where tactics... tree | commitdiff
2004-11-04 Andrea AspertiAuto moved to a new file autoTactic.ml tree | commitdiff
2004-11-04 Andrea AspertiNew version(s) of hint. One more stable (hint) and... tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.