From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 16:46:04 +0000 (+0200)
Subject: Made bombs more explosive (strongly)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ade21b2ea3af70e54e030c62f8b46a996f9ca8fb;hp=004af0d4267446f320a99dc9045e50c06f9a787d;p=fireball-separation.git

Made bombs more explosive (strongly)
---

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