elim tactic: it needs two arguments, a term as well as a pattern

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index e8fd2fe022b9c2a72b54f67ba16375c1d41f9586..d7ed16efd103aa6cdea44040794c135c4fac44ef 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 (_, pattern, using, num, idents) ->
-      sprintf "elim %s%s%s" 
-      (pp_tactic_pattern pattern)
+  | 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_tactic_pattern pattern)
       (pp_intros_specs (num, idents)) 
   | ElimType (_, term, using, num, idents) ->
       sprintf "elim type " ^ term_pp term ^