Amend coqchk description for rewrite rules

coq · Feb 16, 2024 · 7ba8516 · 7ba8516
1 parent 3b9768f
commit 7ba8516
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
@@ -29,7 +29,7 @@ let pr_impredicative_set env =
   else str "Theory: Set is predicative"
 
 let pr_rewrite_rules env =
-  if rewrite_rules_allowed env then str "Theory: Rewrite rules are allowed (subject reduction might be broken)"
+  if rewrite_rules_allowed env then str "Theory: Rewrite rules are allowed (consistency, subject reduction, confluence and normalization might be broken)"
   else str "Theory: Rewrite rules are not allowed"
 
 let pr_assumptions ass axs =