X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Ftactics%2FintroductionTactics.ml;h=9751b2b7478fdf0d05dc74ea092fbfc1b60c6774;hb=a6fc115fd7d4cfba94a43f001f4c27322d3db1a8;hp=b425f219af8585778f7b1a1bcc27fd57c774be39;hpb=d651bf2e3d560e194fbe948dd950dd600a40eab6;p=helm.git

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index b425f219a..9751b2b74 100644
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -23,8 +23,7 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let constructor_tac ~n ~status:(proof, goal) =
+let constructor_tac ~n (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
@@ -34,27 +33,12 @@ let constructor_tac ~n ~status:(proof, goal) =
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
          PrimitiveTactics.apply_tac 
           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-          ~status:(proof, goal)
+          (proof, goal)
       | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
 ;;
 
-
-let exists_tac ~status =
-  constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
-  constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
-  constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
-  constructor_tac ~n:2 ~status
-;;
+let exists_tac status = constructor_tac ~n:1 status ;;
+let split_tac status = constructor_tac ~n:1 status ;;
+let left_tac status = constructor_tac ~n:1 status ;;
+let right_tac status = constructor_tac ~n:2 status ;;