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 2f012ed40d9eded87bf8fcf62c6c0dd929aafac6..0e063d82b6f60b728b4608715e8a80e75957cd05 100644 (file)
--- 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 =