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

[helm.git] / components / grafite_engine / grafiteEngine.ml

diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml
index db08a6038f86bcf08c23f6fc33ec3994ef79010e..4c177fee76d3c6245ec47091af00f15427c733a7 100644 (file)
--- a/components/grafite_engine/grafiteEngine.ml
+++ b/components/grafite_engine/grafiteEngine.ml
@@ -87,9 +87,9 @@ let tactic_of_ast status ast =
       Tactics.demodulate 
        ~dbd:(LibraryDb.instance ()) ~universe:status.GrafiteTypes.universe
   | GrafiteAst.Destruct (_,term) -> Tactics.destruct term
-  | GrafiteAst.Elim (_, what, using, depth, names) ->
+  | GrafiteAst.Elim (_, pattern, using, depth, names) ->
       Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
-        what
+        pattern
   | GrafiteAst.ElimType (_, what, using, depth, names) ->
       Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
         what