diff --git a/src/library/tactic/CMakeLists.txt b/src/library/old_tactic/tactic/CMakeLists.txt
similarity index 100%
rename from src/library/tactic/CMakeLists.txt
rename to src/library/old_tactic/tactic/CMakeLists.txt
diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/old_tactic/tactic/apply_tactic.cpp
similarity index 100%
rename from src/library/tactic/apply_tactic.cpp
rename to src/library/old_tactic/tactic/apply_tactic.cpp
diff --git a/src/library/tactic/apply_tactic.h b/src/library/old_tactic/tactic/apply_tactic.h
similarity index 100%
rename from src/library/tactic/apply_tactic.h
rename to src/library/old_tactic/tactic/apply_tactic.h
diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/old_tactic/tactic/assert_tactic.cpp
similarity index 100%
rename from src/library/tactic/assert_tactic.cpp
rename to src/library/old_tactic/tactic/assert_tactic.cpp
diff --git a/src/library/tactic/assert_tactic.h b/src/library/old_tactic/tactic/assert_tactic.h
similarity index 100%
rename from src/library/tactic/assert_tactic.h
rename to src/library/old_tactic/tactic/assert_tactic.h
diff --git a/src/library/tactic/change_tactic.cpp b/src/library/old_tactic/tactic/change_tactic.cpp
similarity index 100%
rename from src/library/tactic/change_tactic.cpp
rename to src/library/old_tactic/tactic/change_tactic.cpp
diff --git a/src/library/tactic/change_tactic.h b/src/library/old_tactic/tactic/change_tactic.h
similarity index 100%
rename from src/library/tactic/change_tactic.h
rename to src/library/old_tactic/tactic/change_tactic.h
diff --git a/src/library/tactic/check_expr_tactic.cpp b/src/library/old_tactic/tactic/check_expr_tactic.cpp
similarity index 100%
rename from src/library/tactic/check_expr_tactic.cpp
rename to src/library/old_tactic/tactic/check_expr_tactic.cpp
diff --git a/src/library/tactic/check_expr_tactic.h b/src/library/old_tactic/tactic/check_expr_tactic.h
similarity index 100%
rename from src/library/tactic/check_expr_tactic.h
rename to src/library/old_tactic/tactic/check_expr_tactic.h
diff --git a/src/library/tactic/clear_tactic.cpp b/src/library/old_tactic/tactic/clear_tactic.cpp
similarity index 100%
rename from src/library/tactic/clear_tactic.cpp
rename to src/library/old_tactic/tactic/clear_tactic.cpp
diff --git a/src/library/tactic/clear_tactic.h b/src/library/old_tactic/tactic/clear_tactic.h
similarity index 100%
rename from src/library/tactic/clear_tactic.h
rename to src/library/old_tactic/tactic/clear_tactic.h
diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/old_tactic/tactic/congruence_tactic.cpp
similarity index 100%
rename from src/library/tactic/congruence_tactic.cpp
rename to src/library/old_tactic/tactic/congruence_tactic.cpp
diff --git a/src/library/tactic/congruence_tactic.h b/src/library/old_tactic/tactic/congruence_tactic.h
similarity index 100%
rename from src/library/tactic/congruence_tactic.h
rename to src/library/old_tactic/tactic/congruence_tactic.h
diff --git a/src/library/tactic/constructor_tactic.cpp b/src/library/old_tactic/tactic/constructor_tactic.cpp
similarity index 100%
rename from src/library/tactic/constructor_tactic.cpp
rename to src/library/old_tactic/tactic/constructor_tactic.cpp
diff --git a/src/library/tactic/constructor_tactic.h b/src/library/old_tactic/tactic/constructor_tactic.h
similarity index 100%
rename from src/library/tactic/constructor_tactic.h
rename to src/library/old_tactic/tactic/constructor_tactic.h
diff --git a/src/library/tactic/contradiction_tactic.cpp b/src/library/old_tactic/tactic/contradiction_tactic.cpp
similarity index 100%
rename from src/library/tactic/contradiction_tactic.cpp
rename to src/library/old_tactic/tactic/contradiction_tactic.cpp
diff --git a/src/library/tactic/contradiction_tactic.h b/src/library/old_tactic/tactic/contradiction_tactic.h
similarity index 100%
rename from src/library/tactic/contradiction_tactic.h
rename to src/library/old_tactic/tactic/contradiction_tactic.h
diff --git a/src/library/tactic/elaborate.cpp b/src/library/old_tactic/tactic/elaborate.cpp
similarity index 100%
rename from src/library/tactic/elaborate.cpp
rename to src/library/old_tactic/tactic/elaborate.cpp
diff --git a/src/library/tactic/elaborate.h b/src/library/old_tactic/tactic/elaborate.h
similarity index 100%
rename from src/library/tactic/elaborate.h
rename to src/library/old_tactic/tactic/elaborate.h
diff --git a/src/library/tactic/exact_tactic.cpp b/src/library/old_tactic/tactic/exact_tactic.cpp
similarity index 100%
rename from src/library/tactic/exact_tactic.cpp
rename to src/library/old_tactic/tactic/exact_tactic.cpp
diff --git a/src/library/tactic/exact_tactic.h b/src/library/old_tactic/tactic/exact_tactic.h
similarity index 100%
rename from src/library/tactic/exact_tactic.h
rename to src/library/old_tactic/tactic/exact_tactic.h
diff --git a/src/library/tactic/exfalso_tactic.cpp b/src/library/old_tactic/tactic/exfalso_tactic.cpp
similarity index 100%
rename from src/library/tactic/exfalso_tactic.cpp
rename to src/library/old_tactic/tactic/exfalso_tactic.cpp
diff --git a/src/library/tactic/exfalso_tactic.h b/src/library/old_tactic/tactic/exfalso_tactic.h
similarity index 100%
rename from src/library/tactic/exfalso_tactic.h
rename to src/library/old_tactic/tactic/exfalso_tactic.h
diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/old_tactic/tactic/expr_to_tactic.cpp
similarity index 100%
rename from src/library/tactic/expr_to_tactic.cpp
rename to src/library/old_tactic/tactic/expr_to_tactic.cpp
diff --git a/src/library/tactic/expr_to_tactic.h b/src/library/old_tactic/tactic/expr_to_tactic.h
similarity index 100%
rename from src/library/tactic/expr_to_tactic.h
rename to src/library/old_tactic/tactic/expr_to_tactic.h
diff --git a/src/library/tactic/generalize_tactic.cpp b/src/library/old_tactic/tactic/generalize_tactic.cpp
similarity index 100%
rename from src/library/tactic/generalize_tactic.cpp
rename to src/library/old_tactic/tactic/generalize_tactic.cpp
diff --git a/src/library/tactic/generalize_tactic.h b/src/library/old_tactic/tactic/generalize_tactic.h
similarity index 100%
rename from src/library/tactic/generalize_tactic.h
rename to src/library/old_tactic/tactic/generalize_tactic.h
diff --git a/src/library/tactic/goal.cpp b/src/library/old_tactic/tactic/goal.cpp
similarity index 100%
rename from src/library/tactic/goal.cpp
rename to src/library/old_tactic/tactic/goal.cpp
diff --git a/src/library/tactic/goal.h b/src/library/old_tactic/tactic/goal.h
similarity index 100%
rename from src/library/tactic/goal.h
rename to src/library/old_tactic/tactic/goal.h
diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/old_tactic/tactic/induction_tactic.cpp
similarity index 100%
rename from src/library/tactic/induction_tactic.cpp
rename to src/library/old_tactic/tactic/induction_tactic.cpp
diff --git a/src/library/tactic/induction_tactic.h b/src/library/old_tactic/tactic/induction_tactic.h
similarity index 100%
rename from src/library/tactic/induction_tactic.h
rename to src/library/old_tactic/tactic/induction_tactic.h
diff --git a/src/library/tactic/init_module.cpp b/src/library/old_tactic/tactic/init_module.cpp
similarity index 100%
rename from src/library/tactic/init_module.cpp
rename to src/library/old_tactic/tactic/init_module.cpp
diff --git a/src/library/tactic/init_module.h b/src/library/old_tactic/tactic/init_module.h
similarity index 100%
rename from src/library/tactic/init_module.h
rename to src/library/old_tactic/tactic/init_module.h
diff --git a/src/library/tactic/injection_tactic.cpp b/src/library/old_tactic/tactic/injection_tactic.cpp
similarity index 100%
rename from src/library/tactic/injection_tactic.cpp
rename to src/library/old_tactic/tactic/injection_tactic.cpp
diff --git a/src/library/tactic/injection_tactic.h b/src/library/old_tactic/tactic/injection_tactic.h
similarity index 100%
rename from src/library/tactic/injection_tactic.h
rename to src/library/old_tactic/tactic/injection_tactic.h
diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/old_tactic/tactic/intros_tactic.cpp
similarity index 100%
rename from src/library/tactic/intros_tactic.cpp
rename to src/library/old_tactic/tactic/intros_tactic.cpp
diff --git a/src/library/tactic/intros_tactic.h b/src/library/old_tactic/tactic/intros_tactic.h
similarity index 100%
rename from src/library/tactic/intros_tactic.h
rename to src/library/old_tactic/tactic/intros_tactic.h
diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/old_tactic/tactic/inversion_tactic.cpp
similarity index 100%
rename from src/library/tactic/inversion_tactic.cpp
rename to src/library/old_tactic/tactic/inversion_tactic.cpp
diff --git a/src/library/tactic/inversion_tactic.h b/src/library/old_tactic/tactic/inversion_tactic.h
similarity index 100%
rename from src/library/tactic/inversion_tactic.h
rename to src/library/old_tactic/tactic/inversion_tactic.h
diff --git a/src/library/tactic/location.cpp b/src/library/old_tactic/tactic/location.cpp
similarity index 100%
rename from src/library/tactic/location.cpp
rename to src/library/old_tactic/tactic/location.cpp
diff --git a/src/library/tactic/location.h b/src/library/old_tactic/tactic/location.h
similarity index 100%
rename from src/library/tactic/location.h
rename to src/library/old_tactic/tactic/location.h
diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/old_tactic/tactic/norm_num_tactic.cpp
similarity index 100%
rename from src/library/tactic/norm_num_tactic.cpp
rename to src/library/old_tactic/tactic/norm_num_tactic.cpp
diff --git a/src/library/tactic/norm_num_tactic.h b/src/library/old_tactic/tactic/norm_num_tactic.h
similarity index 100%
rename from src/library/tactic/norm_num_tactic.h
rename to src/library/old_tactic/tactic/norm_num_tactic.h
diff --git a/src/library/tactic/note_tactic.cpp b/src/library/old_tactic/tactic/note_tactic.cpp
similarity index 100%
rename from src/library/tactic/note_tactic.cpp
rename to src/library/old_tactic/tactic/note_tactic.cpp
diff --git a/src/library/tactic/note_tactic.h b/src/library/old_tactic/tactic/note_tactic.h
similarity index 100%
rename from src/library/tactic/note_tactic.h
rename to src/library/old_tactic/tactic/note_tactic.h
diff --git a/src/library/tactic/proof_state.cpp b/src/library/old_tactic/tactic/proof_state.cpp
similarity index 100%
rename from src/library/tactic/proof_state.cpp
rename to src/library/old_tactic/tactic/proof_state.cpp
diff --git a/src/library/tactic/proof_state.h b/src/library/old_tactic/tactic/proof_state.h
similarity index 100%
rename from src/library/tactic/proof_state.h
rename to src/library/old_tactic/tactic/proof_state.h
diff --git a/src/library/tactic/register_module.h b/src/library/old_tactic/tactic/register_module.h
similarity index 100%
rename from src/library/tactic/register_module.h
rename to src/library/old_tactic/tactic/register_module.h
diff --git a/src/library/tactic/relation_tactics.cpp b/src/library/old_tactic/tactic/relation_tactics.cpp
similarity index 100%
rename from src/library/tactic/relation_tactics.cpp
rename to src/library/old_tactic/tactic/relation_tactics.cpp
diff --git a/src/library/tactic/relation_tactics.h b/src/library/old_tactic/tactic/relation_tactics.h
similarity index 100%
rename from src/library/tactic/relation_tactics.h
rename to src/library/old_tactic/tactic/relation_tactics.h
diff --git a/src/library/tactic/rename_tactic.cpp b/src/library/old_tactic/tactic/rename_tactic.cpp
similarity index 100%
rename from src/library/tactic/rename_tactic.cpp
rename to src/library/old_tactic/tactic/rename_tactic.cpp
diff --git a/src/library/tactic/rename_tactic.h b/src/library/old_tactic/tactic/rename_tactic.h
similarity index 100%
rename from src/library/tactic/rename_tactic.h
rename to src/library/old_tactic/tactic/rename_tactic.h
diff --git a/src/library/tactic/replace_tactic.cpp b/src/library/old_tactic/tactic/replace_tactic.cpp
similarity index 100%
rename from src/library/tactic/replace_tactic.cpp
rename to src/library/old_tactic/tactic/replace_tactic.cpp
diff --git a/src/library/tactic/replace_tactic.h b/src/library/old_tactic/tactic/replace_tactic.h
similarity index 100%
rename from src/library/tactic/replace_tactic.h
rename to src/library/old_tactic/tactic/replace_tactic.h
diff --git a/src/library/tactic/revert_tactic.cpp b/src/library/old_tactic/tactic/revert_tactic.cpp
similarity index 100%
rename from src/library/tactic/revert_tactic.cpp
rename to src/library/old_tactic/tactic/revert_tactic.cpp
diff --git a/src/library/tactic/revert_tactic.h b/src/library/old_tactic/tactic/revert_tactic.h
similarity index 100%
rename from src/library/tactic/revert_tactic.h
rename to src/library/old_tactic/tactic/revert_tactic.h
diff --git a/src/library/tactic/rewrite_tactic.cpp b/src/library/old_tactic/tactic/rewrite_tactic.cpp
similarity index 100%
rename from src/library/tactic/rewrite_tactic.cpp
rename to src/library/old_tactic/tactic/rewrite_tactic.cpp
diff --git a/src/library/tactic/rewrite_tactic.h b/src/library/old_tactic/tactic/rewrite_tactic.h
similarity index 100%
rename from src/library/tactic/rewrite_tactic.h
rename to src/library/old_tactic/tactic/rewrite_tactic.h
diff --git a/src/library/tactic/subst_tactic.cpp b/src/library/old_tactic/tactic/subst_tactic.cpp
similarity index 100%
rename from src/library/tactic/subst_tactic.cpp
rename to src/library/old_tactic/tactic/subst_tactic.cpp
diff --git a/src/library/tactic/subst_tactic.h b/src/library/old_tactic/tactic/subst_tactic.h
similarity index 100%
rename from src/library/tactic/subst_tactic.h
rename to src/library/old_tactic/tactic/subst_tactic.h
diff --git a/src/library/tactic/tactic.cpp b/src/library/old_tactic/tactic/tactic.cpp
similarity index 100%
rename from src/library/tactic/tactic.cpp
rename to src/library/old_tactic/tactic/tactic.cpp
diff --git a/src/library/tactic/tactic.h b/src/library/old_tactic/tactic/tactic.h
similarity index 100%
rename from src/library/tactic/tactic.h
rename to src/library/old_tactic/tactic/tactic.h
diff --git a/src/library/tactic/trace_tactic.cpp b/src/library/old_tactic/tactic/trace_tactic.cpp
similarity index 100%
rename from src/library/tactic/trace_tactic.cpp
rename to src/library/old_tactic/tactic/trace_tactic.cpp
diff --git a/src/library/tactic/trace_tactic.h b/src/library/old_tactic/tactic/trace_tactic.h
similarity index 100%
rename from src/library/tactic/trace_tactic.h
rename to src/library/old_tactic/tactic/trace_tactic.h
diff --git a/src/library/tactic/unfold_rec.cpp b/src/library/old_tactic/tactic/unfold_rec.cpp
similarity index 100%
rename from src/library/tactic/unfold_rec.cpp
rename to src/library/old_tactic/tactic/unfold_rec.cpp
diff --git a/src/library/tactic/unfold_rec.h b/src/library/old_tactic/tactic/unfold_rec.h
similarity index 100%
rename from src/library/tactic/unfold_rec.h
rename to src/library/old_tactic/tactic/unfold_rec.h
diff --git a/src/library/tactic/util.cpp b/src/library/old_tactic/tactic/util.cpp
similarity index 100%
rename from src/library/tactic/util.cpp
rename to src/library/old_tactic/tactic/util.cpp
diff --git a/src/library/tactic/util.h b/src/library/old_tactic/tactic/util.h
similarity index 100%
rename from src/library/tactic/util.h
rename to src/library/old_tactic/tactic/util.h
diff --git a/src/library/tactic/with_options_tactic.cpp b/src/library/old_tactic/tactic/with_options_tactic.cpp
similarity index 100%
rename from src/library/tactic/with_options_tactic.cpp
rename to src/library/old_tactic/tactic/with_options_tactic.cpp
diff --git a/src/library/tactic/with_options_tactic.h b/src/library/old_tactic/tactic/with_options_tactic.h
similarity index 100%
rename from src/library/tactic/with_options_tactic.h
rename to src/library/old_tactic/tactic/with_options_tactic.h