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

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

diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml
index c669a4161defd736fde2cdd6d1774b3db095b911..189cd9079b4fd429a330948cbb535b720a3a8593 100644 (file)
--- a/helm/software/components/tactics/declarative.ml
+++ b/helm/software/components/tactics/declarative.ml
@@ -121,18 +121,38 @@ let we_need_to_prove t id ty =
       ProofEngineTypes.mk_tactic aux
 ;;
 
-let existselim t id1 t1 id2 t2 =
-(*BUG: t1 and t2 not used *)
-(*PARSING BUG: t2 is parsed in the current context, but it may
-  have occurrences of id1 in it *)
- Tactics.elim_intros t
-  ~mk_fresh_name_callback:
-    (let i = ref 0 in
-      fun _ _ _  ~typ ->
-       incr i;
-       if !i = 1 then Cic.Name id1 else Cic.Name id2)
+let existselim ~dbd ~universe t id1 t1 id2 t2 =
+ let aux (proof, goal) = 
+  let (n,metasenv,bo,ty,attrs) = proof in
+  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 
+        ~mk_fresh_name_callback:
+          (let i = ref 0 in
+            fun _ _ _  ~typ ->
+             incr i;
+             if !i = 1 then Cic.Name id1 else Cic.Name id2) ;
+       (match t with
+          None -> Tactics.auto ~dbd ~params:[] ~universe
+        | Some t -> Tactics.apply t)
+     ]) (proof', goal)
+ in
+  ProofEngineTypes.mk_tactic aux
+;;
 
-let andelim = existselim;;
+let andelim t id1 t1 id2 t2 = 
+ Tactics.elim_intros (ProofEngineTypes.conclusion_pattern (Some t))
+      ~mk_fresh_name_callback:
+        (let i = ref 0 in
+          fun _ _ _  ~typ ->
+           incr i;
+           if !i = 1 then Cic.Name id1 else Cic.Name id2)
 
 let rewritingstep ~dbd ~universe lhs rhs just last_step =
  let aux ((proof,goal) as status) =
@@ -231,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 =