X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FeliminationTactics.ml;h=27cb1cc33cacf6663db8ec41a6f6edb12c76a858;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bb269411ede2ec4749dba9a456d8dbc020a7fc56;hpb=8b55faddb06e3c4b0a13839210bb49170939b33e;p=helm.git

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index bb269411e..27cb1cc33 100644
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -103,16 +103,19 @@ let elim_clear_tac ~mk_fresh_name_callback ~types ~what =
 
 (* 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 ****************************************************************)