Bug in mk_app with C

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