From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 31 May 2007 15:02:14 +0000 (+0000)
Subject: Ferruccio has changed the semantics of the old ~pattern argument of elim_tac.
X-Git-Tag: make_still_working~6267
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f94fdc754f1fb4d9e9feeaf2fdab15481cfadd91;p=helm.git

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.
---

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index 2f012ed40..0e063d82b 100644
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -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 =