]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
beginning of the tactics lapply and fwd
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index b9babaa65a7e5b4b47f7b0da9ea70603525b82d9..e86f77bd6e998f41035e8548763a4326b16ecf17 100644 (file)
@@ -101,6 +101,7 @@ let rec pp_tactic = function
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ pp_term_ast term
+  | FwdSimpl (_, ident) -> sprintf "fwd %s" ident
 
 let pp_flavour = function
   | `Definition -> "Definition"