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/nnAuto.ml

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

2010-03-31	Andrea Asperti	Tracing mechanism for auto. Interface changed to solve...	blob \| commitdiff \| raw
2010-03-24	Claudio Sacerdoti...	Axioms were not indexed.	blob \| commitdiff \| raw \| diff to current
2010-03-24	Andrea Asperti	Computation of the trace.	blob \| commitdiff \| raw \| diff to current
2010-03-18	Andrea Asperti	Printings removed.	blob \| commitdiff \| raw \| diff to current
2010-03-18	Andrea Asperti	Debugging disabled.	blob \| commitdiff \| raw \| diff to current
2010-03-18	Andrea Asperti	New demodulation tactics (mostly for debugging purposes).	blob \| commitdiff \| raw \| diff to current
2010-03-18	Andrea Asperti	app of app inside smart application.	blob \| commitdiff \| raw \| diff to current
2010-03-16	Claudio Sacerdoti...	1) intros cleans up the cache (because the context...	blob \| commitdiff \| raw \| diff to current
2010-03-16	Claudio Sacerdoti...	refreshing of inferred type was missing	blob \| commitdiff \| raw \| diff to current
2010-03-12	Andrea Asperti	Subst was missing in perforate small (apparently, gty...	blob \| commitdiff \| raw \| diff to current
2010-03-04	Andrea Asperti	1. For smart application, we only perforate small terms...	blob \| commitdiff \| raw \| diff to current
2010-02-19	Andrea Asperti	Open goals fixed (it also returned closed goals).	blob \| commitdiff \| raw \| diff to current
2010-02-19	Andrea Asperti	Removed debug printings.	blob \| commitdiff \| raw \| diff to current
2010-02-19	Andrea Asperti	added lazy	blob \| commitdiff \| raw \| diff to current
2010-02-19	Andrea Asperti	Nuova versione di auto.	blob \| commitdiff \| raw \| diff to current
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	blob \| commitdiff \| raw \| diff to current
2010-02-15	Claudio Sacerdoti...	The height of fixpoint applications was not computed...	blob \| commitdiff \| raw \| diff to current
2010-02-11	Enrico Tassi	minimal sequent height set to 1	blob \| commitdiff \| raw \| diff to current
2010-02-11	Enrico Tassi	some experiment filtering with height	blob \| commitdiff \| raw \| diff to current
2010-02-08	Andrea Asperti	Removed debug printings.	blob \| commitdiff \| raw \| diff to current
2010-02-01	Andrea Asperti	On the last goal at maxdepth we stop at the first solution.	blob \| commitdiff \| raw \| diff to current
2010-01-29	Andrea Asperti	Nuova gestione della width.	blob \| commitdiff \| raw \| diff to current
2010-01-18	Andrea Asperti	New paramod tac.	blob \| commitdiff \| raw \| diff to current
2010-01-08	Andrea Asperti	Support for the new // tactics.	blob \| commitdiff \| raw \| diff to current
2009-12-21	Andrea Asperti	Refining with no expected type + unification seems...	blob \| commitdiff \| raw \| diff to current
2009-12-21	Andrea Asperti	Trying to be faster.	blob \| commitdiff \| raw \| diff to current
2009-12-10	Andrea Asperti	Minor bag fixed, relative to failures.	blob \| commitdiff \| raw \| diff to current
2009-12-10	Andrea Asperti	A compiling version?	blob \| commitdiff \| raw \| diff to current
2009-12-09	Andrea Asperti	Attached fast_eq_check to auto	blob \| commitdiff \| raw \| diff to current
2009-12-04	Andrea Asperti	Indexing local context for paramod.	blob \| commitdiff \| raw \| diff to current
2009-11-23	Andrea Asperti	Subsumption and reduction	blob \| commitdiff \| raw \| diff to current
2009-11-17	Andrea Asperti	Closing the goal.	blob \| commitdiff \| raw \| diff to current
2009-11-13	Andrea Asperti	Added the new auto version (not attached yet).	blob \| commitdiff \| raw \| diff to current

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

RSS Atom