subst tactic put in a file on its own

[helm.git] / components / tactics / declarative.ml

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 110f72fb1fb4c5fb511be332f50ff552e858c539..6c37acaa4fdfa1ae224ef2d5ae7945570a6e0cac 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -250,8 +250,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- (*BUG here: pat unused *)
- Tactics.elim_intros ~depth:0 t
+ let pattern = None, [], Some pat in
+ Tactics.elim_intros ~depth:0 ~pattern t
 ;;
 
 let case id ~params =