From: acondolu <andrea.condoluci@unibo.it>
Date: Mon, 11 Jun 2018 14:39:05 +0000 (+0200)
Subject: Fix bug traces of old constructor B
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ad332f3befc4922498db7a9ca6dbb7cc67dbf75b;p=fireball-separation.git

Fix bug traces of old constructor B
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 154992d..9de1f2a 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -115,7 +115,7 @@ let rec no_leading_lambdas v n = 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 -> let t = subst (level + 1) delift sub t in if t = B then B else L t
+ | L t -> L (subst (level + 1) delift sub t)
  | A (t1,t2) ->
   let t1 = subst level delift sub t1 in
   let t2 = subst level delift sub t2 in