]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Fix lifting bug in unwind
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 23:05:17 +0000 (01:05 +0200)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2018 23:05:42 +0000 (01:05 +0200)
problems/simple.* now pass

ocaml/pure.ml

index e04b4eac7baedccd62054516e58068087178f5fa..be08bb4ae3086086e704824d2636c9d843c38409 100644 (file)
@@ -75,7 +75,7 @@ let unwind ?(tbl = Hashtbl.create 317) m =
     | V n ->
        (try
          lift l (cache_unwind (List.nth e (n - l)))
-        with Failure _ -> V (n - l))
+        with Failure _ -> V n)
     | L t -> L (aux (l+1) t)
     | B -> B in
   let t = aux 0 t in