From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 13 Oct 2004 08:06:10 +0000 (+0000)
Subject: pretty printed Absurd's term
X-Git-Tag: V_0_0_10~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=844c8ec10832e5b03456b622db240e18ce014a57;p=helm.git

pretty printed Absurd's term
---

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) ->