]> matita.cs.unibo.it Git - helm.git/history - matita/components/ng_tactics/nDestructTac.ml
Use of standard OCaml syntax
[helm.git] / matita / components / ng_tactics / nDestructTac.ml
2023-01-02 Claudio Sacerdoti... Use of standard OCaml syntax
2019-10-18 Ferruccio GuidiMerge remote-tracking branch 'origin/ld-0.99.3'
2019-10-01 Ferruccio GuidiMerge remote-tracking branch 'origin/matita-lablgtk3'
2019-09-27 Claudio Sacerdoti... Merge branch 'declarative' into matita-lablgtk3
2019-09-27 Claudio Sacerdoti... Most warnings turned into errors and avoided
2018-12-27 Claudio Sacerdoti... Most warnings turned into errors and avoided
2013-02-01 Ferruccio Guidi- ng_refiner:
2012-10-08 Wilmer RicciottiDowngrades buggy destruct patch.
2012-10-05 Wilmer RicciottiRemoves debug prints that were left from last commit.
2012-10-05 Wilmer RicciottiThis patch allows generation of minimally dependent...
2012-05-30 Ferruccio Guidi- nDestructTac: Sys.break handled in two places
2011-11-25 Ferruccio Guidibugfix in clearing the replaced variable: a relocation...
2011-11-24 Ferruccio GuidiDestruct: we warn about the substituted variable to...
2011-11-24 Ferruccio Guidi- now destruct tries to clear the replaced variables...
2011-10-20 Wilmer RicciottiRemoved some unneeded normalizations from the generatio...
2011-10-18 Wilmer RicciottiChanges in "destruct" tactic (allowing performance...
2011-10-11 Claudio Sacerdoti... New version (by Wilmer). The main difference w.r.t...
2011-10-10 Claudio Sacerdoti... 1. nInversion/nDestruct ported to work with jmeq properly
2011-07-15 Claudio Sacerdoti... The name of the constructor for jmeq changed.
2011-01-11 Claudio Sacerdoti... HUGE COMMIT:
2010-10-08 Andrea AsperticicNotation* ==> notation*
2010-09-30 Claudio Sacerdoti... Stuff moved from old Matita.