-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) ;;