* http://cs.unibo.it/helm/.
*)
+(* $Id$ *)
+
module C = Cic
module P = PrimitiveTactics
module T = Tacticals
module F = FreshNamesGenerator
module E = ProofEngineTypes
module H = ProofEngineHelpers
-module Q = MetadataQuery
(*
let induction_tac ~term status =
(* elim type ****************************************************************)
-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 in
- let elim_type_tac status =
- let tac = T.thens ~start: (P.cut_tac what)
- ~continuations:[elim (C.Rel 1); T.id_tac]
- in
- E.apply_tactic tac status
- in
- E.mk_tactic elim_type_tac
+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
+ in
+ let elim_type_tac status =
+ let tac =
+ T.thens ~start: (P.cut_tac what) ~continuations:[elim (C.Rel 1); T.id_tac]
+ in
+ E.apply_tactic tac status
+ in
+ E.mk_tactic elim_type_tac
(* decompose ****************************************************************)
let (proof, goal) = status in
let _, metasenv,_,_ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
- let types = List.rev_append user_types (Q.decomposables dbd) in
+ let types = List.rev_append user_types (FwdQueries.decomposables dbd) in
let tactic = elim_clear_tac ~mk_fresh_name_callback ~types in
let old_context_length = List.length context in
let tac = T.then_ ~start:(tactic ~what)