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-03-22	Claudio Sacerdoti...	Bug fixed in assumption_tac: a missing (lift n) when...	blob \| commitdiff \| raw
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