diff --git a/src/tactic/smtlogics/qfaufbv_tactic.h b/src/tactic/smtlogics/qfaufbv_tactic.h
index d4503a5de..1e4a7419f 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.h
+++ b/src/tactic/smtlogics/qfaufbv_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("qfaufbv",  "builtin strategy for solving QF_AUFBV problems.", "mk_qfaufbv_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/tactic/smtlogics/qfauflia_tactic.h b/src/tactic/smtlogics/qfauflia_tactic.h
index 10b790e70..fbf19fec0 100644
--- a/src/tactic/smtlogics/qfauflia_tactic.h
+++ b/src/tactic/smtlogics/qfauflia_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("qfauflia",  "builtin strategy for solving QF_AUFLIA problems.", "mk_qfauflia_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/tactic/smtlogics/qfidl_tactic.h b/src/tactic/smtlogics/qfidl_tactic.h
index f502dbd89..f892bb8a5 100644
--- a/src/tactic/smtlogics/qfidl_tactic.h
+++ b/src/tactic/smtlogics/qfidl_tactic.h
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+    ADD_TACTIC("qfidl", "builtin strategy for solving QF_IDL problems.", "mk_qfidl_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/tactic/smtlogics/qfuf_tactic.h b/src/tactic/smtlogics/qfuf_tactic.h
index 732e1289f..0c81ad57b 100644
--- a/src/tactic/smtlogics/qfuf_tactic.h
+++ b/src/tactic/smtlogics/qfuf_tactic.h
@@ -26,4 +26,8 @@ class tactic;
 
 tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p);
 
+/*
+  ADD_TACTIC("qfuf", "builtin strategy for solving QF_UF problems.", "mk_qfuf_tactic(m, p)")
+*/
+
 #endif
diff --git a/src/tactic/smtlogics/qfufbv_tactic.h b/src/tactic/smtlogics/qfufbv_tactic.h
index e9ffe4dc3..ceb125517 100644
--- a/src/tactic/smtlogics/qfufbv_tactic.h
+++ b/src/tactic/smtlogics/qfufbv_tactic.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Tactic for QF_UFBV 
+    Tactic for QF_UFBV
 
 Author:
 
@@ -25,4 +25,8 @@ class tactic;
 
 tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
+/*
+  ADD_TACTIC("qfufbv", "builtin strategy for solving QF_UFBV problems.", "mk_qfufbv_tactic(m, p)")
+*/
+
 #endif