X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Ftacticals.ml;h=06f96a573c28f367c244a649080c4fc136c7e981;hb=f438e9b0c8e43a66c56b17adeb8793042d0aade1;hp=f3f7793032365bb5194137002b9356e0a2a80881;hpb=57e3de08d963ff08d671c639c0e9990368b86f20;p=helm.git diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml index f3f779303..06f96a573 100644 --- a/helm/software/components/tactics/tacticals.ml +++ b/helm/software/components/tactics/tacticals.ml @@ -113,7 +113,7 @@ struct back to obtain the result of the tactic *) let mk_tactic f = PET.mk_tactic - (fun (proof, goal) as pstatus -> + (fun ((proof, goal) as pstatus) -> let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in let istatus = pstatus, stack in let (proof, _, _), stack = f istatus in