From f6999a487d16f6b6111429d722bedca76d343c2a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 9 Oct 2007 11:01:34 +0000 Subject: [PATCH] added patch to allow i,j,k: skip and *: skip --- components/tactics/continuationals.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/components/tactics/continuationals.ml b/components/tactics/continuationals.ml index d90e10019..044fa45c8 100644 --- a/components/tactics/continuationals.ml +++ b/components/tactics/continuationals.ml @@ -72,7 +72,8 @@ struct let is_open = function _, Open _ -> true | _ -> false let close = function n, Open g -> n, Closed g | l -> l let filter_open = List.filter is_open - let is_fresh = function n, Open _ when n > 0 -> true | _ -> false + let is_fresh = + function n, Open _ when n > 0 -> true | _,Closed _ -> true | _ -> false let goal_of_loc = function _, Open g | _, Closed g -> g let goal_of_switch = function Open g | Closed g -> g let switch_of_loc = snd -- 2.39.2