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

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

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 189cd9079b4fd429a330948cbb535b720a3a8593..6c37acaa4fdfa1ae224ef2d5ae7945570a6e0cac 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -127,12 +127,11 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
   let metano,context,_ = CicUtil.lookup_meta goal metasenv in
   let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
   let proof' = (n,metasenv,bo,ty,attrs) in
-   let pattern = ProofEngineTypes.conclusion_pattern (Some (Cic.Rel 1)) in
    ProofEngineTypes.apply_tactic (
    Tacticals.thens
     ~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
     ~continuations:
-     [ Tactics.elim_intros pattern 
+     [ Tactics.elim_intros (Cic.Rel 1)
         ~mk_fresh_name_callback:
           (let i = ref 0 in
             fun _ _ _  ~typ ->
@@ -147,7 +146,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
 ;;
 
 let andelim t id1 t1 id2 t2 = 
- Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
+ Tactics.elim_intros t
       ~mk_fresh_name_callback:
         (let i = ref 0 in
           fun _ _ _  ~typ ->
@@ -251,8 +250,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- let pattern = Some (fun c m u -> t, m, u), [], Some pat in
- Tactics.elim_intros ~depth:0 pattern
+ let pattern = None, [], Some pat in
+ Tactics.elim_intros ~depth:0 ~pattern t
 ;;
 
 let case id ~params =