diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index 37b77ef52..e4c71341a 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -53,15 +53,24 @@ def extract_tactic_doc(ous, f):
             if is_doc.search(line):
                 generate_tactic_doc(ous, f, ins)
 
+def presort_files():
+    tac_files = []
+    for root, dirs, files in os.walk(doc_path("../src")):
+        for f in files:
+            if f.endswith("tactic.h"):
+                tac_files += [(f, os.path.join(root, f))]
+    tac_files = sorted(tac_files, key = lambda x: x[0])
+    return tac_files
+    
 def help(ous):
+    presort_files()
     ous.write("---\n")
     ous.write("title: Tactics Summary\n")
     ous.write("sidebar_position: 5\n")
     ous.write("---\n")
-    for root, dirs, files in os.walk(doc_path("../src")):
-        for f in files:
-            if f.endswith("tactic.h"):
-                extract_tactic_doc(ous, os.path.join(root, f))
+    tac_files = presort_files()
+    for file, path in tac_files:
+        extract_tactic_doc(ous, path)
 
 def mk_dir(d):
     if not os.path.exists(d):
diff --git a/src/ast/simplifiers/card2bv.cpp b/src/ast/simplifiers/card2bv.cpp
index b2fece21e..d2d482aa3 100644
--- a/src/ast/simplifiers/card2bv.cpp
+++ b/src/ast/simplifiers/card2bv.cpp
@@ -55,7 +55,7 @@ void card2bv::collect_statistics(statistics& st) const {
 }
 
 void card2bv::collect_param_descrs(param_descrs& r) {
-    r.insert("keep_cardinality_constraints", CPK_BOOL, "(default: true) retain cardinality constraints for solver");
+    r.insert("keep_cardinality_constraints", CPK_BOOL, "retain cardinality constraints for solver", "true");
     pb2bv_rewriter rw(m, m_params);
     rw.collect_param_descrs(r);
 }
diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h
index d28326514..f3cd4e2c8 100644
--- a/src/tactic/arith/card2bv_tactic.h
+++ b/src/tactic/arith/card2bv_tactic.h
@@ -11,7 +11,7 @@ Author:
 
 Tactic Documentation:
 
-## Tactic car2bv
+## Tactic card2bv
 
 ### Short Description