diff --git a/src/tactic/ufbv/macro_finder_tactic.h b/src/tactic/ufbv/macro_finder_tactic.h
index 560f89b23..2c8048b10 100644
--- a/src/tactic/ufbv/macro_finder_tactic.h
+++ b/src/tactic/ufbv/macro_finder_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_macro_finder_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("macro-finder",  "Identifies and applies macros.", "mk_macro_finder_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/tactic/ufbv/quasi_macros_tactic.h b/src/tactic/ufbv/quasi_macros_tactic.h
index c09771761..b654c3e4e 100644
--- a/src/tactic/ufbv/quasi_macros_tactic.h
+++ b/src/tactic/ufbv/quasi_macros_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_quasi_macros_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("quasi-macros",  "Identifies and applies quasi-macros.", "mk_quasi_macros_tactic(m, p)")
+*/
+
 #endif