Made bombs more explosive (strongly)

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 41b7372b471e12e87d7514a286b917c730fcf478..07cf670c134c75c5787c332302ca1b8c265fa186 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -106,16 +106,17 @@ let rec get_inert = function
 let rec subst level delift sub =\r
  function\r
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)\r
- | L t -> L (subst (level + 1) delift sub t)\r
+ | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t\r
  | A (t1,t2) ->\r
   let t1 = subst level delift sub t1 in\r
   let t2 = subst level delift sub t2 in\r
   mk_app t1 t2\r
  | B -> B\r
-and mk_app t1 t2 = if t1 = delta && t2 = delta then B else match t1 with\r
- | B | _ when t2 = B -> B\r
+and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
+ else match t1 with\r
+ | B -> B\r
  | L t1 -> subst 0 true (0, t2) t1\r
- | t1 -> A (t1, t2)\r
+ | _ -> A (t1, t2)\r
 and lift n =\r
  let rec aux lev =\r
   function\r
@@ -158,6 +159,7 @@ let rec purify = function
 ;;\r
 \r
 let check p sigma =\r
+ print_endline "Checking...";\r
  let div = purify p.div in\r
  let conv = purify p.conv in\r
  let sigma = List.map (fun (v,t) -> v, purify t) sigma in\r