X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=17d416ea98405720fbcebb3e1303f2c6501b2394;hb=33581c2ba6d8414968f4d3375352526ebf831a68;hp=27cb1cc33cacf6663db8ec41a6f6edb12c76a858;hpb=9e8c5d2163e701413517153f00a52dac1cd31ecd;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index 27cb1cc33..17d416ea9 100644
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -30,7 +30,6 @@ module S = ProofEngineStructuralRules
 module F = FreshNamesGenerator
 module E = ProofEngineTypes
 module H = ProofEngineHelpers
-module Q = MetadataQuery
 
 (*
 let induction_tac ~term status =
@@ -147,7 +146,7 @@ let decompose_tac ?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[])
       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)