]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
bumped changelog line to match upload date
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index e98e7acfefefc6d446033f0bca45b2abd357f46b..76f1bbd5623961fa624a52e7253ba41027130d77 100644 (file)
@@ -40,6 +40,7 @@ let rec pp_tactic = function
   | 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)
@@ -88,6 +89,8 @@ let pp_flavour = function
 
 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 ->