Skip to content

Commit 9696e45

Browse files
Merge PR rocq-prover#20365: Small simplification in debug_print_modtab
Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
2 parents a5a4966 + d3b892f commit 9696e45

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

vernac/declaremods.ml

+3-3
Original file line numberDiff line numberDiff line change
@@ -742,11 +742,11 @@ let rec get_module_sobjs is_mod env inl = function
742742

743743
let debug_print_modtab () =
744744
let pr_seg = function
745-
| [] -> str "[]"
746-
| l -> str "[." ++ int (List.length l) ++ str ".]"
745+
| 0 -> str "[]"
746+
| l -> str "[." ++ int l ++ str ".]"
747747
in
748748
let pr_modinfo mp modobjs s =
749-
let objs = List.map ignore modobjs.module_substituted_objects @ List.map ignore modobjs.module_keep_objects.keep_objects in
749+
let objs = List.length modobjs.module_substituted_objects + List.length modobjs.module_keep_objects.keep_objects in
750750
s ++ str (ModPath.to_string mp) ++ spc () ++ pr_seg objs
751751
in
752752
let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in

0 commit comments

Comments
 (0)