matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/variousTactics.ml

]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics/variousTactics.ml

[helm.git] / helm / ocaml / tactics / variousTactics.ml

2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw
2005-09-08	Stefano Zacchiroli	implemented lazy disambiguation of tactics arguments...	blob \| commitdiff \| raw \| diff to current
2005-07-09	Claudio Sacerdoti...	Some terms were processed in the wrong context.	blob \| commitdiff \| raw \| diff to current
2005-07-09	Claudio Sacerdoti...	Generalize ported to the new select up to unification.	blob \| commitdiff \| raw \| diff to current
2005-07-08	Claudio Sacerdoti...	1. PrimitiveTactics.new_metasenv_for_apply changed...	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	Obsolete comment removed.	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	Stupid bug fixed (a completely erroneous assert false...	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	This commit makes ProofEngineHelpers.select reach its...	blob \| commitdiff \| raw \| diff to current
2005-06-29	Claudio Sacerdoti...	1. new syntax for patterns:	blob \| commitdiff \| raw \| diff to current
2005-06-27	Claudio Sacerdoti...	A few other tactics made available to matita.	blob \| commitdiff \| raw \| diff to current
2005-06-27	Enrico Tassi	1) moved select and pattern_of from cicUtil to proofEng...	blob \| commitdiff \| raw \| diff to current
2005-06-23	Claudio Sacerdoti...	Tactic generalize ported to patterns and activated...	blob \| commitdiff \| raw \| diff to current
2005-04-27	Stefano Zacchiroli	merged changes from the svn fork by me and Enrico	blob \| commitdiff \| raw \| diff to current
2005-03-22	Claudio Sacerdoti...	Bug fixed in assumption_tac: a missing (lift n) when...	blob \| commitdiff \| raw \| diff to current
2004-12-01	Enrico Tassi	Added universes handling. The PRE_UNIVERSES tag may...	blob \| commitdiff \| raw \| diff to current
2004-11-29	Stefano Zacchiroli	passes ~subst to FreshNameGenerator	blob \| commitdiff \| raw \| diff to current
2004-11-04	Andrea Asperti	Auto moved to a new file autoTactic.ml	blob \| commitdiff \| raw \| diff to current
2004-11-03	Stefano Zacchiroli	no longer use Dbi module but directly use Mysql module...	blob \| commitdiff \| raw \| diff to current
2004-10-22	Stefano Zacchiroli	- reimplemented tacticChaser and friends in term of...	blob \| commitdiff \| raw \| diff to current
2004-10-21	Stefano Zacchiroli	fixed a buggy pattern matching	blob \| commitdiff \| raw \| diff to current
2004-07-05	Stefano Zacchiroli	commented out some debugging instructions	blob \| commitdiff \| raw \| diff to current
2004-07-01	Stefano Zacchiroli	New handling of substitution:	blob \| commitdiff \| raw \| diff to current
2004-06-01	Enrico Tassi	new universes implementation	blob \| commitdiff \| raw \| diff to current
2004-05-21	Matteo Selmi	Added a sort function to decide the order of theorems...	blob \| commitdiff \| raw \| diff to current
2004-05-18	Andrea Asperti	Nuova implementazione di Auto "breadth-first".	blob \| commitdiff \| raw \| diff to current
2004-05-17	Matteo Selmi	Added a filter for uris in tactic "auto".	blob \| commitdiff \| raw \| diff to current
2004-05-10	Andrea Asperti	Adding file match_concl	blob \| commitdiff \| raw \| diff to current
2004-04-20	Stefano Zacchiroli	got rid of ~status label so that tactics can now be...	blob \| commitdiff \| raw \| diff to current
2004-04-14	Claudio Sacerdoti...	Bug fixed: the following happened.	blob \| commitdiff \| raw \| diff to current
2004-03-12	acerioni	First implementation of the Auto tactic.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	fresh_name_generator has now also the metasenv parameter.	blob \| commitdiff \| raw \| diff to current
2004-02-05	Claudio Sacerdoti...	mk_fresh_name moved to FreshNamesGenerator.	blob \| commitdiff \| raw \| diff to current
2004-01-27	Stefano Zacchiroli	s/List.find.../CicUtil.lookup_meta/	blob \| commitdiff \| raw \| diff to current
2003-09-05	Claudio Sacerdoti...	Defs in context may now have an optional type (when...	blob \| commitdiff \| raw \| diff to current
2003-06-19	Claudio Sacerdoti...	Merge of the V7_3_new_exportation branch.	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom