]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5544713) | patch
Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2007 15:02:14 +0000 (15:02 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2007 15:02:14 +0000 (15:02 +0000)
commitf94fdc754f1fb4d9e9feeaf2fdab15481cfadd91
tree8a266597c398d60a910eafa7a38ca0a78f1a46d5tree | snapshot
parent55447138554f33c8588eb836d32ccce2402a09a3commit | diff
Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
However, he did not fix by_induction_tac accordingly. For now I comment out
the ~pattern application. To be fixed.
helm/software/components/tactics/declarative.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.