matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng

]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_tactics

[helm.git] / helm / software / components / ng_tactics /

2010-05-04	Wilmer Ricciotti	* Fixed a couple of glitches in ndestruct	tree \| commitdiff
2010-04-19	Andrea Asperti	Elimination of recursive inductive types leads to looping.	tree \| commitdiff
2010-04-13	Enrico Tassi	auto destructs while introducing in the context	tree \| commitdiff
2010-04-09	Andrea Asperti	apply_subst_context on statuses	tree \| commitdiff
2010-04-08	Claudio Sacerdoti...	New code (unbranched) to compute all keys by all possib...	tree \| commitdiff
2010-04-08	Andrea Asperti	Fixing indexing (commit parziale di Claudio?)	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	Bug fixed: the current equation is not always the last...	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	- inversion principles are now generated also for co...	tree \| commitdiff
2010-03-31	Claudio Sacerdoti...	More debugging info from print_tac.	tree \| commitdiff
2010-03-31	Andrea Asperti	Tracing mechanism for auto. Interface changed to solve...	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Equality has one right parameter and thus it's eliminat...	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	tree \| commitdiff
2010-03-24	Claudio Sacerdoti...	...	tree \| commitdiff
2010-03-24	Andrea Asperti	Computation of the trace.	tree \| commitdiff
2010-03-18	Andrea Asperti	Printings removed.	tree \| commitdiff
2010-03-18	Andrea Asperti	Debugging disabled.	tree \| commitdiff
2010-03-18	Andrea Asperti	New demodulation tactics (mostly for debugging purposes).	tree \| commitdiff
2010-03-18	Andrea Asperti	app of app inside smart application.	tree \| commitdiff
2010-03-17	Ferruccio Guidi	dr	tree \| commitdiff
2010-03-17	Claudio Sacerdoti...	OCaml's inferred type simplified.	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	1) intros cleans up the cache (because the context...	tree \| commitdiff
2010-03-16	Claudio Sacerdoti...	refreshing of inferred type was missing	tree \| commitdiff
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	tree \| commitdiff
2010-03-12	Andrea Asperti	removed debug from the inteface	tree \| commitdiff
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	tree \| commitdiff
2010-03-02	Wilmer Ricciotti	Added syntax for ninversion tactic (still experimental).	tree \| commitdiff
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	tree \| commitdiff
2010-02-19	Andrea Asperti	Removed debug printings.	tree \| commitdiff
2010-02-19	Andrea Asperti	added lazy	tree \| commitdiff
2010-02-19	Andrea Asperti	Nuova versione di auto.	tree \| commitdiff
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	tree \| commitdiff
2010-02-15	Claudio Sacerdoti...	The height of fixpoint applications was not computed...	tree \| commitdiff
2010-02-11	Enrico Tassi	minimal sequent height set to 1	tree \| commitdiff
2010-02-11	Enrico Tassi	some experiment filtering with height	tree \| commitdiff
2010-02-08	Andrea Asperti	Removed debug printings.	tree \| commitdiff
2010-02-03	Wilmer Ricciotti	Disabled debug prints in ndestruct tactic.	tree \| commitdiff
2010-02-02	Wilmer Ricciotti	New version using Streicher's K axiom. Should be faster...	tree \| commitdiff
2010-02-02	Wilmer Ricciotti	Fixed a bug with indexed inductive types which sometime...	tree \| commitdiff
2010-02-01	Andrea Asperti	On the last goal at maxdepth we stop at the first solution.	tree \| commitdiff
2010-01-29	Andrea Asperti	Nuova gestione della width.	tree \| commitdiff
2010-01-18	Andrea Asperti	New paramod tac.	tree \| commitdiff
2010-01-18	Andrea Asperti	Invocation of paramod	tree \| commitdiff
2010-01-18	Andrea Asperti	paramod_tac exported	tree \| commitdiff
2010-01-12	Wilmer Ricciotti	Fixed a bug in the discrimination principle: the refine...	tree \| commitdiff
2010-01-08	Andrea Asperti	Support for the new // tactics.	tree \| commitdiff
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	tree \| commitdiff
2009-12-21	Andrea Asperti	Trying to be faster.	tree \| commitdiff
2009-12-10	Andrea Asperti	Minor bag fixed, relative to failures.	tree \| commitdiff
2009-12-10	Andrea Asperti	A compiling version?	tree \| commitdiff
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	tree \| commitdiff
2009-12-09	Andrea Asperti	Added nnAuto.mli	tree \| commitdiff
2009-12-04	Wilmer Ricciotti	Bugfix in inversion (was using refl_eq instead of refl).	tree \| commitdiff
2009-12-04	Andrea Asperti	Indexing local context for paramod.	tree \| commitdiff
2009-11-27	Wilmer Ricciotti	ndestruct now clears off identity equations whenever...	tree \| commitdiff
2009-11-25	Wilmer Ricciotti	Fixed inversion, which was broken by the last changes...	tree \| commitdiff
2009-11-23	Andrea Asperti	Subsumption and reduction	tree \| commitdiff
2009-11-17	Wilmer Ricciotti	ndestruct tactic: mainly bugfixes; the algorithm isn...	tree \| commitdiff
2009-11-17	Andrea Asperti	Closing the goal.	tree \| commitdiff
2009-11-16	Wilmer Ricciotti	Implementation of ndestruct tactic (including destructi...	tree \| commitdiff
2009-11-13	Andrea Asperti	Added the new auto version (not attached yet).	tree \| commitdiff
2009-11-12	Claudio Sacerdoti...	Code made more uniform.	tree \| commitdiff
2009-11-04	Claudio Sacerdoti...	Bug fixed: restrict used to take the list of positions...	tree \| commitdiff
2009-11-04	Claudio Sacerdoti...	1) sort computation undone (it used to be bugged anyway)	tree \| commitdiff
2009-10-30	Enrico Tassi	auto snapshot	tree \| commitdiff
2009-10-28	Claudio Sacerdoti...	Bug fixed: the `IsTerm attribute is now added by mk_met...	tree \| commitdiff
2009-10-28	Enrico Tassi	better indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	better indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	better comments and indentation	tree \| commitdiff
2009-10-28	Enrico Tassi	use prop_only to filter instead of repeting the same...	tree \| commitdiff
2009-10-28	Enrico Tassi	better logging	tree \| commitdiff
2009-10-28	Enrico Tassi	better logging and immediate pruning of new goals when	tree \| commitdiff
2009-10-28	Enrico Tassi	auto navigates a real tree, not a flattened one	tree \| commitdiff
2009-10-28	Enrico Tassi	labels in group_by_tac	tree \| commitdiff
2009-10-28	Enrico Tassi	new data structures for auto	tree \| commitdiff
2009-10-28	Enrico Tassi	export group_by_tac	tree \| commitdiff
2009-10-23	Enrico Tassi	added code to print the tree	tree \| commitdiff
2009-10-23	Enrico Tassi	more functions	tree \| commitdiff
2009-10-22	Enrico Tassi	new instantiate, only known bug is w.r.t. in/out scope...	tree \| commitdiff
2009-10-21	Enrico Tassi	first bits for the zipper	tree \| commitdiff
2009-10-21	Enrico Tassi	...	tree \| commitdiff
2009-10-21	Enrico Tassi	more printings	tree \| commitdiff
2009-10-21	Enrico Tassi	nauto:	tree \| commitdiff
2009-10-19	Claudio Sacerdoti...	Smarter implementation of instantiate to avoid re-check...	tree \| commitdiff
2009-10-16	Enrico Tassi	some work for auto	tree \| commitdiff
2009-10-16	Enrico Tassi	some work for auto	tree \| commitdiff
2009-10-13	Enrico Tassi	relocate is hopefully fixed once and for-all!	tree \| commitdiff
2009-10-13	Enrico Tassi	relocate fixed	tree \| commitdiff
2009-10-13	Enrico Tassi	debug + relocate uses Prop instead of (Prop Prop)....	tree \| commitdiff
2009-10-11	Enrico Tassi	auto with intro	tree \| commitdiff
2009-10-08	Enrico Tassi	removed misleading context	tree \| commitdiff
2009-10-08	Enrico Tassi	new discrimination tree instantiation with	tree \| commitdiff
2009-10-08	Enrico Tassi	avoid warning	tree \| commitdiff
2009-10-07	Enrico Tassi	removed printing	tree \| commitdiff
2009-10-07	Enrico Tassi	short names	tree \| commitdiff
2009-10-07	Enrico Tassi	auto works on the regular tactics status	tree \| commitdiff
2009-10-07	Enrico Tassi	the wrap function takes a string argument so that we...	tree \| commitdiff
2009-10-07	Enrico Tassi	unfocus can be performed also if all goals are closed	tree \| commitdiff
2009-10-07	Claudio Sacerdoti...	Debugging code commented out.	tree \| commitdiff
2009-10-06	Enrico Tassi	fixed constructor on non inductive type	tree \| commitdiff
next

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

RSS Atom