| Abst of bool * N.layer * term (* x-reduced?, layer, type *)
| Abbr of term (* body *)
-and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int (* attrs, position index *)
- | GRef of attrs * uri (* attrs, reference *)
- | Cast of attrs * term * term (* attrs, type, term *)
- | Appl of attrs * term * term (* attrs, argument, function *)
- | Bind of attrs * bind * term (* attrs, binder, scope *)
+and term = Sort of attrs * int (* attrs, hierarchy index *)
+ | LRef of attrs * int (* attrs, position index *)
+ | GRef of attrs * uri (* attrs, reference *)
+ | Cast of attrs * term * term (* attrs, type, term *)
+ | Appl of attrs * bool * term * term (* attrs, extended?, argument, function *)
+ | Bind of attrs * bind * term (* attrs, binder, scope *)
type entity = term E.entity (* attrs, uri, binder *)
(* Currified constructors ***************************************************)
-let abst x n w = Abst (x, n, w)
+let abst r n w = Abst (r, n, w)
let abbr v = Abbr v
let cast a u t = Cast (a, u, t)
-let appl a u t = Appl (a, u, t)
+let appl a x u t = Appl (a, x, u, t)
let bind a b t = Bind (a, b, t)
-let bind_abst x n a u t = Bind (a, Abst (x, n, u), t)
+let bind_abst r n a u t = Bind (a, Abst (r, n, u), t)
let bind_abbr a u t = Bind (a, Abbr u, t)