bumped changelog line to match upload date

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 089f8b896073a256682a0b6428e94295ae9f385d..76f1bbd5623961fa624a52e7253ba41027130d77 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -38,8 +38,9 @@ let pp_reduction_kind = function
 
 let rec pp_tactic = function
   | LocatedTactic (loc, tac) -> pp_tactic tac
-  | Absurd -> "absurd"
+  | 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)
@@ -59,6 +60,7 @@ let rec pp_tactic = function
   | Fold (kind, term) ->
       sprintf "fold %s %s" (pp_reduction_kind kind) (pp_term term)
   | Fourier -> "fourier"
+  | Hint -> "hint"
   | Injection ident -> "injection " ^ ident
   | Intros (num, idents) ->
       sprintf "intros%s%s"
@@ -87,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 ->