X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcontinuationals.ml;fp=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fcontinuationals.ml;h=eeff9f9bf537783b0e859cfc686cbd0e09aa41b9;hb=17974f325b94010f784b745d481bbd343ba59bb1;hp=7ea357e89679694087ce106e890559b4e028d686;hpb=e717c6e032c43b7f56ff9491424cf024b1819fc1;p=helm.git diff --git a/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml index 7ea357e89..eeff9f9bf 100644 --- a/helm/software/components/tactics/continuationals.ml +++ b/helm/software/components/tactics/continuationals.ml @@ -302,7 +302,7 @@ struct debug_print (lazy ("closed: " ^ String.concat " " (List.map string_of_int gcn))); let stack = - (zero_pos gon, t @~- gcn, k @~- gon, tag) :: deep_close gcn s + (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s in sn, stack | Dot, ([], _, [], _) :: _ ->