From f94fdc754f1fb4d9e9feeaf2fdab15481cfadd91 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 31 May 2007 15:02:14 +0000 Subject: [PATCH 1/1] 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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 = -- 2.39.2