X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FintroductionTactics.ml;h=6318f489041d48e02e9590c501c53ff1a9e5cee1;hb=7bf5d654c18fee290e7e402800543fe40223c04b;hp=bc28c41709c92719a143d40506a9db6860a2f8e5;hpb=a3ef256812f0397a871fe8e69c125dfd89e62dce;p=helm.git

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index bc28c4170..6318f4890 100644
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -32,8 +32,9 @@ let constructor_tac ~n ~status:(proof, goal) =
      match (R.whd context ty) with
         (C.MutInd (uri, typeno, exp_named_subst))
       | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
-         PrimitiveTactics.apply_tac ~status:(proof, goal)
+         PrimitiveTactics.apply_tac 
           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
+          ~status:(proof, goal)
       | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
 ;;