X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Ftactics%2Fdeclarative.ml;h=6c37acaa4fdfa1ae224ef2d5ae7945570a6e0cac;hb=e05e28d01c55699ce539699ac745341bfa4c1c0f;hp=110f72fb1fb4c5fb511be332f50ff552e858c539;hpb=dd5b3afb330c2efc69b97cc8762b71bd86685acd;p=helm.git

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 110f72fb1..6c37acaa4 100644
--- 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 =