elim tactic: now takes a pattern instead of just a term

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index e433c9b7b73cf0aa4b261020e8a9287fbe6422af..e8fd2fe022b9c2a72b54f67ba16375c1d41f9586 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -99,10 +99,11 @@ 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 (_, pattern, using, num, idents) ->
+      sprintf "elim %s%s%s" 
+      (pp_tactic_pattern pattern)
       (match using with None -> "" | Some term -> " using " ^ term_pp term)
-      ^ pp_intros_specs (num, idents) 
+      (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)