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: 0.4.95@7852~418
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0c533ab8bc7cd0ad61aad8530dd067202e095c03;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/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 2f012ed40..0e063d82b 100644
--- a/components/tactics/declarative.ml
+++ b/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 =