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 ->
;;
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 ->
;;
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 =