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

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

diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml
index 110f72fb1fb4c5fb511be332f50ff552e858c539..189cd9079b4fd429a330948cbb535b720a3a8593 100644 (file)
--- a/components/tactics/declarative.ml
+++ b/components/tactics/declarative.ml
@@ -127,11 +127,12 @@ 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 (Cic.Rel 1)
+     [ Tactics.elim_intros pattern 
         ~mk_fresh_name_callback:
           (let i = ref 0 in
             fun _ _ _  ~typ ->
@@ -146,7 +147,7 @@ let existselim ~dbd ~universe t id1 t1 id2 t2 =
 ;;
 
 let andelim t id1 t1 id2 t2 = 
- Tactics.elim_intros t
+ Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
       ~mk_fresh_name_callback:
         (let i = ref 0 in
           fun _ _ _  ~typ ->
@@ -250,8 +251,8 @@ let we_proceed_by_cases_on t pat =
 ;;
 
 let we_proceed_by_induction_on t pat =
- (*BUG here: pat unused *)
- Tactics.elim_intros ~depth:0 t
+ let pattern = Some (fun c m u -> t, m, u), [], Some pat in
+ Tactics.elim_intros ~depth:0 pattern
 ;;
 
 let case id ~params =