module F = FreshNamesGenerator
module E = ProofEngineTypes
module H = ProofEngineHelpers
-module Q = MetadataQuery
(*
let induction_tac ~term status =
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)