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

[helm.git] / components / acic_procedural / proceduralTypes.ml

diff --git a/components/acic_procedural/proceduralTypes.ml b/components/acic_procedural/proceduralTypes.ml
index 91f2408b94ba6ea9c15d5e6fee582381a6536a5d..3ef27ea4020392e83173ee70dbc0d8af52247f69 100644 (file)
--- a/components/acic_procedural/proceduralTypes.ml
+++ b/components/acic_procedural/proceduralTypes.ml
@@ -86,7 +86,7 @@ type step = Note of note
          | Cut of name * what * note
          | LetIn of name * what * note
          | Rewrite of how * what * where * pattern * note
-         | Elim of what * using option * note
+         | Elim of what * using option * pattern * note
          | Apply of what * note
          | Change of inferred * what * where * pattern * note 
          | ClearBody of name * note
@@ -137,8 +137,9 @@ let mk_rewrite direction what where pattern =
    let tactic = G.Rewrite (floc, direction, what, pattern, rename) in
    mk_tactic tactic
 
-let mk_elim what using =
-   let tactic = G.Elim (floc, what, using, Some 0, []) in
+let mk_elim what using pattern =
+   let pattern = Some what, [], Some pattern in
+   let tactic = G.Elim (floc, pattern, using, Some 0, []) in
    mk_tactic tactic
 
 let mk_apply t =
@@ -178,7 +179,7 @@ let rec render_step sep a = function
    | Cut (n, t, s)           -> mk_note s :: cont sep (mk_cut n t :: a)
    | LetIn (n, t, s)         -> mk_note s :: cont sep (mk_letin n t :: a)
    | Rewrite (b, t, w, e, s) -> mk_note s :: cont sep (mk_rewrite b t w e :: a)
-   | Elim (t, xu, s)         -> mk_note s :: cont sep (mk_elim t xu :: a)
+   | Elim (t, xu, e, s)      -> mk_note s :: cont sep (mk_elim t xu e :: a)
    | Apply (t, s)            -> mk_note s :: cont sep (mk_apply t :: a)
    | Change (t, _, w, e, s)  -> mk_note s :: cont sep (mk_change t w e :: a)
    | ClearBody (n, s)        -> mk_note s :: cont sep (mk_clearbody n :: a)