New argument (the hypothesis name) for cut.

[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 eeaa500cde0b3d18e44bf9121d34e44321a29a02..bbb2c935b7e8233f47a4f214ad22dcc441ae244e 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -70,7 +70,9 @@ let rec pp_tactic = function
   | Compare (_,term) -> "compare " ^ pp_term_ast term
   | Constructor (_,n) -> "constructor " ^ string_of_int n
   | Contradiction _ -> "contradiction"
-  | Cut (_, term) -> "cut " ^ pp_term_ast term
+  | Cut (_, ident, term) ->
+     "cut " ^ pp_term_ast term ^
+      (match ident with None -> "" | Some id -> " as " ^ id)
   | DecideEquality _ -> "decide equality"
   | Decompose (_, term) ->
       sprintf "decompose %s" (pp_term_ast term)