X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralTypes.ml;h=b4d88169af438c267948b0c382114856ad2b9c05;hb=b4027b84fae91e907b6874060b91d89b6a1ad780;hp=3ef27ea4020392e83173ee70dbc0d8af52247f69;hpb=8ae990161006978a019f0afda4ff8d56a78d1fd0;p=helm.git

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index 3ef27ea40..b4d88169a 100644
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/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 =