* 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
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)
+ ProofEngineTypes.apply_tactic (
+ PrimitiveTactics.apply_tac
+ ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)))
+ (proof, goal)
| _ -> raise (ProofEngineTypes.Fail "Constructor: failed")
;;
+let constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n)
-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 = 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) ;;