Package: ssreflect Severity: wishlist >From upstream VCS:
------------------------------------------------------------------------ r1875 | gonthier | 2010-03-17 12:22:08 +0100 (Wed, 17 Mar 2010) | 4 lines off-by-1 bug that delayed short-circuit occurrence selection: move: {1}(f x) actually looked for two instances of f x, selecting only the first one, insetad of interrupting the search after the first one ------------------------------------------------------------------------ The attached patch fixes the issue. Also note that it's preserving the semantics of commands, just making them more efficient. -- System Information: Debian Release: squeeze/sid APT prefers unstable APT policy: (500, 'unstable'), (500, 'testing'), (1, 'experimental') Architecture: amd64 (x86_64) Kernel: Linux 2.6.34-1-amd64 (SMP w/2 CPU cores)
Index: ssreflect-1.2+dfsg/src/ssreflect.ml =================================================================== --- ssreflect-1.2+dfsg.orig/src/ssreflect.ml 2010-06-21 14:04:33.000000000 +0200 +++ ssreflect-1.2+dfsg/src/ssreflect.ml 2010-06-21 14:04:57.000000000 +0200 @@ -2685,9 +2685,10 @@ let subst_occ = let occ_set = Array.make max_occ (not use_occ) in let _ = List.iter (fun i -> occ_set.(i - 1) <- use_occ) occ_list in + let _ = if max_occ = 0 then skip_occ := use_occ in fun () -> incr nocc; - if !nocc <= max_occ then occ_set.(!nocc - 1) else - begin skip_occ := use_occ; not use_occ end in + if !nocc = max_occ then skip_occ := use_occ; + if !nocc <= max_occ then occ_set.(!nocc - 1) else not use_occ in let rec subst_loop h c' = if !skip_occ then c' else let f, a = splay_app ise c' in