]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics/tactics.ml
Very experimental commit: the type of the source is now required in LetIns
[helm.git] / helm / software / components / tactics / tactics.ml
2008-03-10 Claudio Sacerdoti... Tactic reduce got rid of. Use normalize, instead.
2007-11-06 Ferruccio Guidinew implementation of the destruct tactic,
2007-06-13 Enrico Tassimany changes:
2007-06-01 Enrico Tassinew compose tactic, still undocumented.
2007-05-24 Enrico Tassiauto and autogui... some work
2007-04-20 Claudio Sacerdoti... Much ado about nothing:
2007-04-16 Ferruccio Guidisubst tactic put in a file on its own
2007-01-24 Ferruccio GuidimatitaGui: some missing cases during disambiguation...
2006-12-29 Ferruccio Guidi- tactics:
2006-12-20 Claudio Sacerdoti... New tactic cases (still to be documented).
2006-10-20 Andrea AspertiDemodulate and applyS moved form saturation to auto.
2006-09-27 Enrico Tassiauto snapshot
2006-09-27 Claudio Sacerdoti... Initial work on setoids:
2006-09-25 Claudio Sacerdoti... injection_tac and discriminate_tac now replaced by...
2006-08-28 Ferruccio Guidi- Level-1: some fixes to the extraction procedure
2006-06-15 Andrea Aspertiadded applyS
2006-02-08 Claudio Sacerdoti... Never implemented tactics compare and decide equality...
2006-02-03 Stefano Zacchiroli- renamed ocaml/ to components/