matita.cs.unibo.it Git - helm.git/history

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

2005-06-17	Enrico Tassi	added 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 Asperti	A cleaned version of auto_tac_new.	tree \| commitdiff
2005-06-16	Stefano Zacchiroli	added depth and width (optional) parameters to auto_tac_new	tree \| commitdiff
2005-06-15	Ferruccio Guidi	beginning of the tactics lapply and fwd	tree \| commitdiff
2005-06-15	Enrico Tassi	apply_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 Tassi	paths trough terms implemented with a nice hack :)	tree \| commitdiff
2005-06-01	Enrico Tassi	removed debug prerr_endline	tree \| commitdiff
2005-05-31	Enrico Tassi	added comment	tree \| commitdiff
2005-05-31	Enrico Tassi	implemented normalize (used in new_metasenv_for_apply)	tree \| commitdiff
2005-05-31	Enrico Tassi	fix	tree \| commitdiff
2005-05-30	Andrea Asperti	added intros n	tree \| commitdiff
2005-05-27	Enrico Tassi	removed debug prerr_endline	tree \| commitdiff
2005-05-25	Enrico Tassi	apply now tries both to reduce and to not reduce the...	tree \| commitdiff
2005-05-24	Enrico Tassi	reverted to ==	tree \| commitdiff
2005-05-24	Enrico Tassi	new simpl semantic (now = and not == since you can...	tree \| commitdiff
2005-05-24	Enrico Tassi	added lost elim_intros_tac	tree \| commitdiff
2005-05-24	Andrea Asperti	Added a new tactic elim_intros (without simpl of the...	tree \| commitdiff
2005-05-20	Andrea Asperti	Added a whd on ty in new_metasenv for apply, in order...	tree \| commitdiff
2005-05-20	Andrea Asperti	Hint repaired (an erroneous commit by myself).	tree \| commitdiff
2005-05-19	Stefano Zacchiroli	commented out some debugging messages	tree \| commitdiff
2005-05-17	Enrico Tassi	aded comment	tree \| commitdiff
2005-05-17	Stefano Zacchiroli	bugfix in elim, cardinality constraint should >= 1...	tree \| commitdiff
2005-05-16	Enrico Tassi	fixed instance	tree \| commitdiff
2005-05-13	Alberto Griggio	exported new_metasenv_for_apply, needed by the paramodu...	tree \| commitdiff
2005-05-06	Enrico Tassi	factorization of rewrite.	tree \| commitdiff
2005-05-05	Andrea Asperti	Some modifications due to instance.	tree \| commitdiff
2005-05-03	Enrico Tassi	added sqlStatements module (contains all CREATE TABLE...	tree \| commitdiff
2005-05-03	Enrico Tassi	fix for instance	tree \| commitdiff
2005-05-03	Andrea Asperti	First version of instance.	tree \| commitdiff
2005-05-02	Enrico Tassi	attached auto	tree \| commitdiff
2005-04-29	Enrico Tassi	main constants set is closed with constants types	tree \| commitdiff
2005-04-29	Stefano Zacchiroli	added rating parameter to at_least (used by elim)	tree \| commitdiff
2005-04-27	Stefano Zacchiroli	merged changes from the svn fork by me and Enrico	tree \| commitdiff
2005-04-22	Stefano Zacchiroli	removed debugging print	tree \| commitdiff
2005-04-22	Stefano Zacchiroli	uses 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 Tassi	locate 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 Tassi	new metadataTypes interface (with ownerize function)	tree \| commitdiff
2005-02-01	Enrico Tassi	reverder change. no more owner passed to the locate.	tree \| commitdiff
2005-02-01	Enrico Tassi	added owner support to the disambiguator (now locate...	tree \| commitdiff
2005-01-21	Stefano Zacchiroli	- attributes support	tree \| commitdiff
2005-01-17	Enrico Tassi	new cicEnvironment implementation	tree \| commitdiff
2004-12-06	Andrea Asperti	New version of auto with "width".	tree \| commitdiff
2004-12-03	Stefano Zacchiroli	changed "locate" so that it supports shell-like pattern...	tree \| commitdiff
2004-12-02	Stefano Zacchiroli	* empty log message *	tree \| commitdiff
2004-12-01	Enrico Tassi	Added universes handling. The PRE_UNIVERSES tag may...	tree \| commitdiff
2004-11-30	Andrea Asperti	Bug in the management of substitutions into auto corrected.	tree \| commitdiff
2004-11-29	Stefano Zacchiroli	passes ~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 Asperti	Auto moved to a new file autoTactic.ml	tree \| commitdiff
2004-11-04	Andrea Asperti	New version(s) of hint. One more stable (hint) and...	tree \| commitdiff
2004-11-03	Stefano Zacchiroli	no longer use Dbi module but directly use Mysql module...	tree \| commitdiff
2004-10-25	Stefano Zacchiroli	sort 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 Zacchiroli	added vars selection boolean on locate	tree \| commitdiff
2004-10-22	Andrea Asperti	implemented elim query	tree \| commitdiff
2004-10-22	Andrea Asperti	bugfix: 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 Asperti	ported to typed explicit subst	tree \| commitdiff
2004-10-21	Stefano Zacchiroli	added reference to MetadataQuery (now it builds properly)	tree \| commitdiff
2004-10-21	Stefano Zacchiroli	implemented in place old Filter_auto filtering	tree \| commitdiff
2004-10-21	Stefano Zacchiroli	fixed a buggy pattern matching	tree \| commitdiff
2004-10-20	Stefano Zacchiroli	top level query module	tree \| commitdiff
2004-10-12	Stefano Zacchiroli	setting goal doesn't change history status	tree \| commitdiff
2004-10-04	Stefano Zacchiroli	splitted History module out of StatefulProofEngine	tree \| commitdiff
2004-10-04	Stefano Zacchiroli	- splitted out History module	tree \| commitdiff
2004-09-20	Stefano Zacchiroli	added initial_status	tree \| commitdiff
2004-09-01	Andrea Asperti	Bug fixing: the call to MQueryMisc.wrong_xpointer_forma...	tree \| commitdiff
2004-07-13	Matteo Selmi	Modified filtering function	tree \| commitdiff
2004-07-05	Stefano Zacchiroli	commented 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 Zacchiroli	New handling of substitution:	tree \| commitdiff
2004-06-28	Andrea Asperti	fixed typo	tree \| commitdiff
2004-06-18	Matteo Selmi	Corrections 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 Tassi	fix for proofEngineTypes.mli	tree \| commitdiff
2004-06-01	Enrico Tassi	new universes implementation	tree \| commitdiff
2004-05-31	Matteo Selmi	New filtering function for "Auto" tactic using "just...	tree \| commitdiff
2004-05-25	Matteo Selmi	written a new sort function to postpone the resolution...	tree \| commitdiff
2004-05-21	Matteo Selmi	Added a sort function to decide the order of theorems...	tree \| commitdiff
2004-05-18	Andrea Asperti	Nuova 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 Selmi	Added a filter for uris in tactic "auto".	tree \| commitdiff
2004-05-17	Stefano Zacchiroli	first check in of statefulProofEngine	tree \| commitdiff
2004-05-13	Ferruccio Guidi	- some code patched	tree \| commitdiff
2004-05-13	Stefano Zacchiroli	changed proofStatus so that uri component is optional...	tree \| commitdiff
2004-05-10	Andrea Asperti	Adding file newConstraint	tree \| commitdiff
2004-05-10	Andrea Asperti	Adding file match_concl	tree \| commitdiff
2004-04-23	Enrico Tassi	Universes introduction	tree \| commitdiff
2004-04-22	Claudio Sacerdoti...	Patches to generate ?1 : ?2 : Type in place of ?1 ...	tree \| commitdiff
next

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

RSS Atom