]> matita.cs.unibo.it Git - helm.git/commitdiff
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)
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

index 2f012ed40d9eded87bf8fcf62c6c0dd929aafac6..0e063d82b6f60b728b4608715e8a80e75957cd05 100644 (file)
@@ -257,7 +257,7 @@ let we_proceed_by_cases_on t pat =
 
 let we_proceed_by_induction_on t pat =
  let pattern = None, [], Some pat in
- Tactics.elim_intros ~depth:0 ~pattern t
+ Tactics.elim_intros ~depth:0 (*~pattern*) t
 ;;
 
 let case id ~params =