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

[helm.git] / components / tactics / eliminationTactics.ml

diff --git a/components/tactics/eliminationTactics.ml b/components/tactics/eliminationTactics.ml
index e74886e95e1146235ef0114fd3b350d4360a5e13..85eade2d08e0291ac53b7a5cab724f47b4831e26 100644 (file)
--- a/components/tactics/eliminationTactics.ml
+++ b/components/tactics/eliminationTactics.ml
@@ -127,9 +127,10 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
       let _, metasenv, _, _, _ = proof in
       let _, context, _ = CicUtil.lookup_meta goal metasenv in
       let index, ty = H.lookup_type metasenv context what in
+      let pattern = PET.conclusion_pattern (Some (C.Rel index)) in
       let tac = 
          if check_type sorts metasenv context (S.lift index ty) then 
-            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback (C.Rel index))
+            T.then_ ~start:(P.elim_intros_tac ~mk_fresh_name_callback pattern)
                    ~continuation:(PESR.clear [what])
         else 
            let msg = "unexported elim_clear: not an decomposable type" in
@@ -144,12 +145,13 @@ let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
 let elim_type_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) ?depth
   ?using what
 =
-  let elim what =
-    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback what
+  let elim =
+    P.elim_intros_simpl_tac ?using ?depth ~mk_fresh_name_callback
   in
   let elim_type_tac status =
+    let pattern = PET.conclusion_pattern (Some (C.Rel 1)) in
     let tac =
-      T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+      T.thens ~start: (P.cut_tac what) ~continuations:[elim pattern; T.id_tac]
     in
     PET.apply_tactic tac status
   in