X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=75977662bf3e29b638bf93c397ba6ed5fd35a0b6;hb=1e61e4290c96600e3758b30b660712514ba379e3;hp=089f8b896073a256682a0b6428e94295ae9f385d;hpb=9e67c082f0021849b411ec8acbd041137f1fb73a;p=helm.git diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml index 089f8b896..75977662b 100644 --- a/helm/ocaml/cic_transformations/tacticAstPp.ml +++ b/helm/ocaml/cic_transformations/tacticAstPp.ml @@ -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) ->