elim tactic: it needs two arguments, a term as well as a pattern

[helm.git] / components / acic_procedural / proceduralTypes.ml

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index 3ef27ea4020392e83173ee70dbc0d8af52247f69..b4d88169af438c267948b0c382114856ad2b9c05 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -138,8 +138,8 @@ let mk_rewrite direction what where pattern =
    mk_tactic tactic
 
 let mk_elim what using pattern =
-   let pattern = Some what, [], Some pattern in
-   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
+   let pattern = None, [], Some pattern in
+   let tactic = G.Elim (floc, what, using, pattern, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =