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

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

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

2005-11-18	Claudio Sacerdoti...	Improvement/bug fix: rewriting in the hypothesis used...	blob \| commitdiff \| raw
2005-11-17	Claudio Sacerdoti...	Comments changed/removed.	blob \| commitdiff \| raw \| diff to current
2005-11-17	Claudio Sacerdoti...	"Parallel" rewriting in a list of hypothesis and in...	blob \| commitdiff \| raw \| diff to current
2005-11-17	Claudio Sacerdoti...	Major code semplification and improvement:	blob \| commitdiff \| raw \| diff to current
2005-11-17	Claudio Sacerdoti...	First draft implementation of rewriting in an hypothesis.	blob \| commitdiff \| raw \| diff to current
2005-10-25	Claudio Sacerdoti...	Every exception that used to have type string is now...	blob \| commitdiff \| raw \| diff to current
2005-09-13	Claudio Sacerdoti...	Two bugs fixed in the apply tactic:	blob \| commitdiff \| raw \| diff to current
2005-09-08	Stefano Zacchiroli	implemented lazy disambiguation of tactics arguments...	blob \| commitdiff \| raw \| diff to current
2005-07-08	Claudio Sacerdoti...	Replace is now working again and it is able to match...	blob \| commitdiff \| raw \| diff to current
2005-07-08	Claudio Sacerdoti...	Cosmetic changes: a piece of code replaced with a pre...	blob \| commitdiff \| raw \| diff to current
2005-07-08	Claudio Sacerdoti...	Bug fixed: metavariables generated by the saturation...	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-07-04	Claudio Sacerdoti...	New command default "foo" uri1 ... urin	blob \| commitdiff \| raw \| diff to current
2005-07-02	Claudio Sacerdoti...	All the equalityTactics have now been ported to use...	blob \| commitdiff \| raw \| diff to current
2005-07-01	Claudio Sacerdoti...	replace tactic reimplemented.	blob \| commitdiff \| raw \| diff to current
2005-07-01	Claudio Sacerdoti...	The replace tactic is now working again. It can now...	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	The rewrite_* set of tactics is now working again....	blob \| commitdiff \| raw \| diff to current
2005-06-30	Claudio Sacerdoti...	1. rewrite_* and rewrite_back_* merged into one function	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-24	Enrico Tassi	now we use rplace_lifting_csc since the what must NOT...	blob \| commitdiff \| raw \| diff to current
2005-06-17	Enrico Tassi	added support for goal patterns	blob \| commitdiff \| raw \| diff to current
2005-05-06	Enrico Tassi	factorization of rewrite.	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-06-01	Enrico Tassi	new universes implementation	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-02-24	Claudio Sacerdoti...	Partial porting to V8 URIs.	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
2004-01-22	Stefano Zacchiroli	moved hard coded uris to HelmLibraryObjects	blob \| commitdiff \| raw \| diff to current
2003-12-02	Ferruccio Guidi	sort CProp added	blob \| commitdiff \| raw \| diff to current
2003-09-05	Claudio Sacerdoti...	Replace is now working also over Type.	blob \| commitdiff \| raw \| diff to current
2003-09-05	Claudio Sacerdoti...	Replace tactic fixed. It was not working any longer...	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