added some lines to compile for debugging

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

diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml
index 4cd6bf62ff477db6033aafcd9eeb9e82871fbbe8..e42c3ba513ed2d9e1e1993616f1336337f2a9f56 100644 (file)
--- a/components/tactics/auto.ml
+++ b/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 =