better simplify

[helm.git] / helm / software / components / grafite / grafiteAstPp.ml

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index e433c9b7b73cf0aa4b261020e8a9287fbe6422af..d7ed16efd103aa6cdea44040794c135c4fac44ef 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -99,10 +99,12 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
       sprintf "decompose%s" (pp_intros_specs (None, names)) 
   | Demodulate _ -> "demodulate"
   | Destruct (_, term) -> "destruct " ^ term_pp term
-  | Elim (_, term, using, num, idents) ->
-      sprintf "elim " ^ term_pp term ^
+  | Elim (_, what, using, pattern, num, idents) ->
+      sprintf "elim %s%s %s%s" 
+      (term_pp what)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
-      ^ pp_intros_specs (num, idents) 
+      (pp_tactic_pattern pattern)
+      (pp_intros_specs (num, idents)) 
   | ElimType (_, term, using, num, idents) ->
       sprintf "elim type " ^ term_pp term ^
       (match using with None -> "" | Some term -> " using " ^ term_pp term)