-let push2 err f lenv attr ?t () = match lenv, t with
- | EBind (e, a, Abst ws), Some t -> f (EBind (e, (attr :: a), Abst (t :: ws)))
- | EBind (e, a, Abbr vs), Some t -> f (EBind (e, (attr :: a), Abbr (t :: vs)))
- | EBind (e, a, Void n), None -> f (EBind (e, (attr :: a), Void (succ n)))
- | _ -> err ()
+let push2 err f lenv ?attr ?t () = match lenv, attr, t with
+ | EBind (e, a, Abst (n, ws)), Some attr, Some t ->
+ f (EBind (e, (attr :: a), Abst (n, t :: ws)))
+ | EBind (e, a, Abst (n, ws)), None, Some t ->
+ f (EBind (e, a, Abst (n, t :: ws)))
+ | EBind (e, a, Abbr vs), Some attr, Some t ->
+ f (EBind (e, (attr :: a), Abbr (t :: vs)))
+ | EBind (e, a, Abbr vs), None, Some t ->
+ f (EBind (e, a, Abbr (t :: vs)))
+ | EBind (e, a, Void n), Some attr, None ->
+ f (EBind (e, (attr :: a), Void (succ n)))
+ | EBind (e, a, Void n), None, None ->
+ f (EBind (e, a, Void (succ n)))
+ | _ -> err ()