X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fandrea.ml;h=07cf670c134c75c5787c332302ca1b8c265fa186;hb=ade21b2ea3af70e54e030c62f8b46a996f9ca8fb;hp=dcc954e099c2008c87a8d6b1c0d118feaa99076b;hpb=7c60aa45d5f4486768b6338e2e5aa411dbec8ad9;p=fireball-separation.git

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index dcc954e..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
@@ -171,7 +173,7 @@ let check p sigma =
 let sanity p =
  print_endline (string_of_problem p); (* non cancellare *)
  if p.conv = B then problem_fail p "p.conv diverged";
- (* if p.div = B then raise (Done p.sigma); *)
+ if p.div = B then raise (Done p.sigma);
  if p.phase = `Two && p.div = delta then raise (Done p.sigma);
  if not (is_inert p.div) then problem_fail p "p.div converged"
 ;;