]> matita.cs.unibo.it Git - helm.git/history - matita/components/ng_tactics/nnAuto.ml
- support for candidates of reducibility continues ...
[helm.git] / matita / components / ng_tactics / nnAuto.ml
2011-12-16 Andrea AspertiIn case paramodulation fails we apply unit equalities.
2011-11-21 Andrea AspertiPassing the right subst and metasenv when indexing...
2011-11-18 Wilmer RicciottiSolves a bug that caused the auto statistics to refer...
2011-11-16 Ferruccio Guidi- lambda_delta: context-free weak head normal forms...
2011-11-15 Andrea Aspertinon-facts local candidates must be applied too in prese...
2011-11-03 Andrea AspertiAt top level, we reindex the local equations for each...
2011-11-02 Andrea AspertiDisabled printings.
2011-11-02 Andrea Asperti--Tre the expected branching with the actual one and
2011-10-28 Andrea Asperti-pplicative_case has been rewritten and simplified;
2011-10-21 Andrea AspertiDisabled debug.
2011-10-20 Andrea AspertiAlternatives are ordered according to the number of...
2011-10-10 Claudio Sacerdoti... 1. nInversion/nDestruct ported to work with jmeq properly
2011-10-10 Claudio Sacerdoti... Debugging code commented out.
2011-10-10 Andrea Asperti- Reintroduction of a failure chache
2011-07-19 Ferruccio Guidi- nnAuto.ml: width overflows are warnings, not errors
2011-06-03 Ferruccio GuidiMax width overflows, which cause auto to fail, are...
2011-03-27 Claudio Sacerdoti... Debugging code commented out.
2011-01-11 Claudio Sacerdoti... HUGE COMMIT:
2010-11-18 Andrea AspertiDebugging disabled
2010-11-18 Andrea Asperti- auto now uses the equality of the new library
2010-10-29 Andrea Asperti- grammar of // changed to move the justification inside;
2010-10-08 Andrea AsperticicNotation* ==> notation*
2010-10-06 Andrea AspertiRemoved nAuto.ml-mli
2010-09-30 Claudio Sacerdoti... Stuff moved from old Matita.