]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
renamed Http_client to Http_user_agent to avoid clashes with Gerd's
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index 089f8b896073a256682a0b6428e94295ae9f385d..e98e7acfefefc6d446033f0bca45b2abd357f46b 100644 (file)
@@ -38,7 +38,7 @@ 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
   | Assumption -> "assumption"
   | Change (t1, t2, where) ->
@@ -59,6 +59,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"