- mk_app b (subst b' level delift sub t1) (subst b' level delift sub t2)\r
-(* b is\r
- - a fresh ref true if we want to create a real application from scratch\r
- - a shared ref true if we substituting in the head of a real application *)\r
-and mk_app b' t1 t2 = if t1 = delta && t2 = delta then raise B\r
+ let special = b = `Duplicate && top && t2 = V (level + var) in\r
+ let t1' = subst (if special then false else top) level delift sub t1 in\r
+ let t2' = subst false level delift sub t2 in\r
+ match b with\r
+ | `Duplicate when special ->\r
+ assert (match t1' with L _ -> false | _ -> true) ;\r
+ (match flag with\r
+ | `Some b when !b -> b := false\r
+ | `Some b ->\r
+ print_string "WARNING! Stepping on a useless argument!";\r
+ ignore(read_line())\r
+ | `Inherit | `Duplicate -> assert false);\r
+ A(flag, t1', erase t2')\r
+ | `Inherit | `Duplicate ->\r
+ let b' = if t2 = V (level + var)\r
+ then (assert (flag <> `Inherit); flag)\r
+ else b in\r
+ assert (match t1' with L _ -> false | _ -> true) ;\r
+ A(b', t1', t2')\r
+ | `Some b' -> mk_app top b' t1' t2'\r
+and mk_app top flag t1 t2 = if t1 = delta && t2 = delta then raise B\r