| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
| FwdSimpl (_, term) -> sprintf "fwd %s" (pp_term_ast term)
- | LApply (_, term_opt, term) ->
- sprintf "lapply %s%s" (pp_term_ast term)
- (match term_opt with | None -> "" | Some t -> " to " ^ pp_term_ast t)
+ | LApply (_, term_opt, term, ident) ->
+ sprintf "lapply %s%s%s" (pp_term_ast term)
+ (match term_opt with None -> "" | Some t -> " to " ^ pp_term_ast t)
+ (match ident with None -> "" | Some id -> " " ^ id)
let pp_flavour = function
| `Definition -> "Definition"