| LocatedTactic (loc, tac) -> pp_tactic tac
| Absurd term -> "absurd" ^ pp_term term
| Apply term -> "apply " ^ pp_term term
+ | Auto -> "auto"
| Assumption -> "assumption"
| Change (t1, t2, where) ->
sprintf "change %s with %s%s" (pp_term t1) (pp_term t2)
let pp_command = function
| Abort -> "Abort"
+ | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
+ | Baseuri None -> "Baseuri"
| Check term -> sprintf "Check %s" (CicAstPp.pp_term term)
| Proof -> "Proof"
| Qed name ->