From 7245ccc4076a799ac50546e70327320a8625b5e8 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 6 Jul 2006 08:18:49 +0000 Subject: [PATCH] fixed *: and n,m: --- .../components/tactics/continuationals.ml | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/helm/software/components/tactics/continuationals.ml b/helm/software/components/tactics/continuationals.ml index eeff9f9bf..a7c624120 100644 --- a/helm/software/components/tactics/continuationals.ml +++ b/helm/software/components/tactics/continuationals.ml @@ -330,6 +330,18 @@ struct (([ loc ], t @+ filter_open g, [],`BranchTag) :: (loc_tl, t', k', tag) :: s)) | Shift, _ -> fail (lazy "can't shift goals here") + | Pos i_s, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + let l_js = List.filter (fun (i, _) -> List.mem i i_s) (g' @+ [loc]) in + new_stack + ((l_js, [], [],`BranchTag) + :: ([ loc ] @+ g' @- l_js, t', k', tag) :: s) + | Pos i_s, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> + let l_js = List.filter (fun (i, pos) -> List.mem i i_s) g' in + new_stack + ((l_js, [], [],`BranchTag) + :: (g' @- l_js, t' @+ filter_open g, k', tag) :: s) +(* | Pos i_s, ([ loc ], [], [],`BranchTag) :: (g', t', k', tag) :: s when is_fresh loc -> let l_js = List.filter (fun (i, _) -> List.mem i i_s) g' in @@ -341,12 +353,24 @@ struct new_stack ((l_js, [], [],`BranchTag) :: (g' @- l_js, t' @+ filter_open g, k', tag) :: s) +*) | Pos _, _ -> fail (lazy "can't use relative positioning here") + | Wildcard, ([ loc ] , t, k, `BranchTag) :: (g', t', k', tag) :: s + when is_fresh loc -> + new_stack + (([loc] @+ g', [], [], `BranchTag) + :: ([], t' @+ k, k', tag) :: s) + | Wildcard, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s -> + new_stack + ((g', [], [], `BranchTag) + :: ([], t' @+ filter_open g @+ k, k', tag) :: s) +(* | Wildcard, (g, t, k, `BranchTag) :: (g', t', k', tag) :: s when g = [] || is_fresh (List.hd g) -> new_stack ((g', [], [], `BranchTag) :: ([], t' @+ filter_open g @+ k, k', tag) :: s) +*) | Wildcard, _ -> fail (lazy "can't use wildcard here") | Merge, (g, t, k,`BranchTag) :: (g', t', k', tag) :: s -> new_stack ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s) -- 2.39.2