From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 16:29:52 +0000 (+0200)
Subject: Bug in mk_app with C
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b529f51389b1a5f2f2e5f035f8c1abdafe5a0a4c;p=fireball-separation.git

Bug in mk_app with C
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index b068791..7be80c4 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -129,7 +129,6 @@ let rec subst level delift sub =
  | B -> B
 and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B
  else match t1 with
- | C _ as t -> t
  | B -> B
  | L t1 -> subst 0 true (0, t2) t1
  | _ -> A (t1, t2)