]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
added Auto and Hint tactic
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index e98e7acfefefc6d446033f0bca45b2abd357f46b..f21aca6ba0c2668cacab3a72d2fc74db88a4af7c 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)