-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 constructor_tac ~n = ProofEngineTypes.mk_tactic (fake_constructor_tac ~n)
+
+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) ;;