X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=e98bcd3c878d6fa597ffda35b85a4ee2e0d4d906;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=0aa33c2db5dd2082e5557b9212cb30cc2c51c380;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index 0aa33c2db..e98bcd3c8 100644
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -23,6 +23,8 @@
  * http://cs.unibo.it/helm/.
  *)
 
+(* $Id$ *)
+
 module C = Cic
 module P = PrimitiveTactics
 module T = Tacticals
@@ -30,7 +32,6 @@ module S = ProofEngineStructuralRules
 module F = FreshNamesGenerator
 module E = ProofEngineTypes
 module H = ProofEngineHelpers
-module Q = MetadataQuery
 
 (*
 let induction_tac ~term status =
@@ -97,22 +98,25 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what =
 	                   ~continuation:(S.clear what)
 	 in
 	 E.apply_tactic tac status
-      else raise (E.Fail "unexported elim_clear: not an eliminable type") 
+      else raise (E.Fail (lazy "unexported elim_clear: not an eliminable type"))
    in
    E.mk_tactic elim_clear_tac
 
 (* 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 ****************************************************************)
 
@@ -144,7 +148,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)