X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FintroductionTactics.ml;h=6bf8ab6c1e37d339c37ac5afaef982fe148c3ea1;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6318f489041d48e02e9590c501c53ff1a9e5cee1;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git

diff --git a/helm/ocaml/tactics/introductionTactics.ml b/helm/ocaml/tactics/introductionTactics.ml
index 6318f4890..6bf8ab6c1 100644
--- a/helm/ocaml/tactics/introductionTactics.ml
+++ b/helm/ocaml/tactics/introductionTactics.ml
@@ -23,38 +23,25 @@
  * http://cs.unibo.it/helm/.
  *)
 
-
-let constructor_tac ~n ~status:(proof, goal) =
+let fake_constructor_tac ~n (proof, goal) =
   let module C = Cic in
   let module R = CicReduction in
    let (_,metasenv,_,_) = proof in
-    let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
      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 
-          ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
-          ~status:(proof, goal)
-      | _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
-;;
-
-
-let exists_tac ~status =
-  constructor_tac ~n:1 ~status
+         ProofEngineTypes.apply_tactic (
+          PrimitiveTactics.apply_tac 
+           ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)))
+           (proof, goal)
+      | _ -> raise (ProofEngineTypes.Fail (lazy "Constructor: failed"))
 ;;
 
+let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n)
 
-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  = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let split_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let left_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:1) ;;
+let right_tac = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n:2) ;;