X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fauto.ml;h=e42c3ba513ed2d9e1e1993616f1336337f2a9f56;hb=55447138554f33c8588eb836d32ccce2402a09a3;hp=4cd6bf62ff477db6033aafcd9eeb9e82871fbbe8;hpb=57e3de08d963ff08d671c639c0e9990368b86f20;p=helm.git

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 4cd6bf62f..e42c3ba51 100644
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1085,7 +1085,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals =