| 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"
let pp_command = function
| Qed _ -> "qed"
+ | Drop _ -> "drop"
| Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
| Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
| Alias (_,s) -> pp_alias s