changed reduction tactics ast

[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 76f1bbd5623961fa624a52e7253ba41027130d77..d0e87b0943e91055f4a4d48bb2091b5703a7d425 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -33,7 +33,7 @@ let pp_idents idents = "[" ^ String.concat "; " idents ^ "]"
 
 let pp_reduction_kind = function
   | `Reduce -> "reduce"
-  | `Simpl -> "simpl"
+  | `Simpl -> "simplify"
   | `Whd -> "whd"
 
 let rec pp_tactic = function
@@ -68,7 +68,16 @@ let rec pp_tactic = function
         (match idents with [] -> "" | idents -> " " ^ pp_idents idents)
   | Left -> "left"
   | LetIn (term, ident) -> sprintf "let %s in %s" (pp_term term) ident
-  | Reduce (_, _, _) -> assert false  (* TODO *)
+  | Reduce (kind, None)
+  | Reduce (kind, Some ([], `Goal)) -> pp_reduction_kind kind
+  | Reduce (kind, Some ([], `Everywhere)) ->
+      sprintf "%s in hyp" (pp_reduction_kind kind)
+  | Reduce (kind, Some (terms, `Goal)) ->
+      sprintf "%s %s" (pp_reduction_kind kind)
+        (String.concat ", " (List.map pp_term terms))
+  | Reduce (kind, Some (terms, `Everywhere)) ->
+      sprintf "%s in hyp %s" (pp_reduction_kind kind)
+        (String.concat ", " (List.map pp_term terms))
   | Reflexivity -> "reflexivity"
   | Replace (t1, t2) -> sprintf "replace %s with %s" (pp_term t1) (pp_term t2)
   | Replace_pattern (_, _) -> assert false  (* TODO *)