]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/tacticAstPp.ml
paths trough terms implemented with a nice hack :)
[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml
index a4ec56deecfc3218e69d364211cbce59c7119539..9882aa0e92b0335f0aef7467116c87e5c14e9c0a 100644 (file)
@@ -41,6 +41,7 @@ let pp_reduction_kind = function
   | `Reduce -> "reduce"
   | `Simpl -> "simplify"
   | `Whd -> "whd"
+  | `Normalize -> "normalize"
 
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term