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

2010-03-31	Claudio Sacerdoti...	Bug fixed: the current equation is not always the last...	blob \| commitdiff \| raw
2010-02-19	Andrea Asperti	Added an implicit parameter to branch_tac to allow...	blob \| commitdiff \| raw \| diff to current
2010-02-03	Wilmer Ricciotti	Disabled debug prints in ndestruct tactic.	blob \| commitdiff \| raw \| diff to current
2010-02-02	Wilmer Ricciotti	New version using Streicher's K axiom. Should be faster...	blob \| commitdiff \| raw \| diff to current
2010-01-12	Wilmer Ricciotti	Fixed a bug in the discrimination principle: the refine...	blob \| commitdiff \| raw \| diff to current
2009-11-27	Wilmer Ricciotti	ndestruct now clears off identity equations whenever...	blob \| commitdiff \| raw \| diff to current
2009-11-17	Wilmer Ricciotti	ndestruct tactic: mainly bugfixes; the algorithm isn...	blob \| commitdiff \| raw \| diff to current

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