]> 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
Bug fixed in generalize: a status was generated with an old metasenv.
[helm.git] / helm / ocaml / tactics /
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
2004-11-03 Stefano Zacchirolino longer use Dbi module but directly use Mysql module... tree | commitdiff
2004-10-25 Stefano Zacchirolisort hint's result accordingly to the "least goal left... tree | commitdiff
2004-10-25 Stefano Zacchiroli- added var selection boolean to locate tree | commitdiff
2004-10-25 Stefano Zacchiroliadded vars selection boolean on locate tree | commitdiff
2004-10-22 Andrea Aspertiimplemented elim query tree | commitdiff
2004-10-22 Andrea Aspertibugfix: handle overflow in powerset cardinality tree | commitdiff
2004-10-22 Stefano Zacchiroli- reimplemented tacticChaser and friends in term of... tree | commitdiff
2004-10-22 Andrea Asperti- added (hack) apply_tac_verbose (for auto) tree | commitdiff
2004-10-22 Andrea Aspertiported to typed explicit subst tree | commitdiff
2004-10-21 Stefano Zacchiroliadded reference to MetadataQuery (now it builds properly) tree | commitdiff
2004-10-21 Stefano Zacchiroliimplemented in place old Filter_auto filtering tree | commitdiff
2004-10-21 Stefano Zacchirolifixed a buggy pattern matching tree | commitdiff
2004-10-20 Stefano Zacchirolitop level query module tree | commitdiff
2004-10-12 Stefano Zacchirolisetting goal doesn't change history status tree | commitdiff
2004-10-04 Stefano Zacchirolisplitted History module out of StatefulProofEngine tree | commitdiff
2004-10-04 Stefano Zacchiroli- splitted out History module tree | commitdiff
2004-09-20 Stefano Zacchiroliadded initial_status tree | commitdiff
2004-09-01 Andrea AspertiBug fixing: the call to MQueryMisc.wrong_xpointer_forma... tree | commitdiff
2004-07-13 Matteo SelmiModified filtering function tree | commitdiff
2004-07-05 Stefano Zacchirolicommented out some debugging instructions tree | commitdiff
2004-07-02 Claudio Sacerdoti... Bug fixed: eta_expand did not perform any recursion... tree | commitdiff
2004-07-01 Stefano ZacchiroliNew handling of substitution: tree | commitdiff
2004-06-28 Andrea Aspertifixed typo tree | commitdiff
2004-06-18 Matteo SelmiCorrections to "auto" tactic tree | commitdiff
2004-06-18 Claudio Sacerdoti... elim_tac rewritten almost entirely. It is now based... tree | commitdiff
2004-06-18 Claudio Sacerdoti... Added new function compare_metasenvs. tree | commitdiff
2004-06-18 Claudio Sacerdoti... Comments changed. tree | commitdiff
2004-06-02 Enrico Tassifix for proofEngineTypes.mli tree | commitdiff
2004-06-01 Enrico Tassinew universes implementation tree | commitdiff
2004-05-31 Matteo SelmiNew filtering function for "Auto" tactic using "just... tree | commitdiff
2004-05-25 Matteo Selmiwritten a new sort function to postpone the resolution... tree | commitdiff
2004-05-21 Matteo SelmiAdded a sort function to decide the order of theorems... tree | commitdiff
2004-05-18 Andrea AspertiNuova implementazione di Auto "breadth-first". tree | commitdiff
2004-05-18 Claudio Sacerdoti... * tactics/Makefile fixed (to remove duplicate .mli... tree | commitdiff
2004-05-17 Matteo SelmiAdded a filter for uris in tactic "auto". tree | commitdiff
2004-05-17 Stefano Zacchirolifirst check in of statefulProofEngine tree | commitdiff
2004-05-13 Ferruccio Guidi- some code patched tree | commitdiff
2004-05-13 Stefano Zacchirolichanged proofStatus so that uri component is optional... tree | commitdiff
2004-05-10 Andrea AspertiAdding file newConstraint tree | commitdiff
2004-05-10 Andrea AspertiAdding file match_concl tree | commitdiff
2004-04-23 Enrico TassiUniverses introduction tree | commitdiff
2004-04-22 Claudio Sacerdoti... Patches to generate ?1 : ?2 : Type in place of ?1 ... tree | commitdiff
2004-04-22 Enrico Tassifourier.mli addedto interface files. tree | commitdiff
2004-04-22 Claudio Sacerdoti... IMPLEMENTATION_FILES now generated from INTERFACE_FILES. tree | commitdiff
2004-04-20 Stefano Zacchiroligot rid of ~status label so that tactics can now be... tree | commitdiff
2004-04-14 Claudio Sacerdoti... Bug fixed: the following happened. tree | commitdiff
2004-04-06 Stefano ZacchiroliThe parser accepts terms with metavariables as statemen... tree | commitdiff
2004-04-06 Stefano Zacchirolibugfix: local context and canonical context previously... tree | commitdiff
2004-04-06 Stefano Zacchirolibugfix: the function that abstract constant occurrences... tree | commitdiff
2004-03-31 Matteo SelmitacticChaser modified to avoid double "apply" and to... tree | commitdiff
2004-03-24 Stefano ZacchiroliCSC: hack to make applications of constants that have... tree | commitdiff
2004-03-12 acerioniFirst implementation of the Auto tactic. tree | commitdiff
2004-02-24 Claudio Sacerdoti... New v8.0 URIs. tree | commitdiff
2004-02-24 Claudio Sacerdoti... Porting URIs to V8.0. tree | commitdiff
2004-02-24 Claudio Sacerdoti... Partial porting to V8 URIs. tree | commitdiff
2004-02-12 Ferruccio Guidinew .depend files tree | commitdiff
2004-02-12 Stefano Zacchiroliremoved some anciente debugging messages tree | commitdiff
2004-02-06 Stefano Zacchiroliadded annotations to Cic.Implicit tree | commitdiff
2004-02-05 Claudio Sacerdoti... fresh_name_generator has now also the metasenv parameter. tree | commitdiff
2004-02-05 Claudio Sacerdoti... mk_fresh_name moved to FreshNamesGenerator. tree | commitdiff
2004-02-02 Stefano Zacchirolichanged prototype of CicMetaSubst.apply_subst* tree | commitdiff
2004-01-27 Stefano Zacchirolis/List.find.../CicUtil.lookup_meta/ tree | commitdiff
2004-01-22 Stefano Zacchirolimoved hard coded uris to HelmLibraryObjects tree | commitdiff
2004-01-22 Stefano Zacchiroliported to cicMetaSubst tree | commitdiff
2003-12-02 Ferruccio Guidisort CProp added tree | commitdiff
2003-10-07 Luca Padovani* removed currified constructors everywhere. A bug... tree | commitdiff
2003-09-05 Claudio Sacerdoti... Replace is now working also over Type. tree | commitdiff
2003-09-05 Claudio Sacerdoti... Replace tactic fixed. It was not working any longer... tree | commitdiff
2003-09-05 Claudio Sacerdoti... Defs in context may now have an optional type (when... tree | commitdiff
2003-09-04 Ferruccio Guidiadded the support for the "Locate Inductive Principles... tree | commitdiff
2003-07-17 Ferruccio Guidi- new generated query "unreferred" implemented at serve... tree | commitdiff
2003-07-02 Ferruccio Guidimathql_generator: new constraint format (more type... tree | commitdiff
2003-06-19 Claudio Sacerdoti... The universe was the one of the complete search, not... tree | commitdiff
2003-06-19 Claudio Sacerdoti... Merge of the V7_3_new_exportation branch. tree | commitdiff
Unnamed repository; edit this file 'description' to name the repository.