Optional callbacks have been added to tactics that need to introduce

[helm.git] / helm / ocaml / tactics / eliminationTactics.ml

diff --git a/helm/ocaml/tactics/eliminationTactics.ml b/helm/ocaml/tactics/eliminationTactics.ml
index ae947f5ec4bd35759702588c95790410d10d07ee..73d1771ff6d0002c0ece8743c09d25fcfac72dc0 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.ml
+++ b/helm/ocaml/tactics/eliminationTactics.ml
@@ -49,7 +49,7 @@ let elim_type_tac ~term ~status =
   let module P = PrimitiveTactics in
   let module T = Tacticals in
    T.thens
-    ~start: (P.cut_tac ~term)
+    ~start: (P.cut_tac term)
     ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
     ~status
 ;;
@@ -96,7 +96,9 @@ let cic_textual_parser_uri_of_string uri' =
   _ -> raise (IllFormedUri uri')
 ;;
 
-let decompose_tac ~term ~uris_choice_callback ~status:((proof,goal) as status) =
+let decompose_tac ?(uris_choice_callback=(function l -> l)) term
+ ~status:((proof,goal) as status)
+=
   let module C = Cic in
   let module R = CicReduction in
   let module P = PrimitiveTactics in