]> matita.cs.unibo.it Git - fireball-separation.git/blobdiff - ocaml/pure.ml
Tentative implementation of strong separation algorithm
[fireball-separation.git] / ocaml / pure.ml
index f1cac843e2349f15c1e5c4cf9c5dd00e3c05e4af..7963f8732132a75bab5620326e1c193278af16ff 100644 (file)
@@ -94,6 +94,7 @@ in
    let rec aux g =
     function
     (* mmm -> print_endline (print_machine mmm); match mmm with *)
+        m when unwind m = let d = L(A(V 0, V 0)) in A(d,d) -> [], B, []
      | (e,A(t1,t2),s) ->
          let t2' = aux g (e,t2,[]) in
          let (_,t,_) = t2' in