Also try without_require=True, insert_at_top=True (#293)

JasonGross · web-flow · commit 886a7fe105bd · 2025-06-25T07:41:09.000Z
diff --git a/coq_tools/find_bug.py b/coq_tools/find_bug.py
@@ -2719,7 +2719,7 @@ def get_test_output(
                 for admit_tactic_wrapper_action in (ADD_ADMIT_TACTIC_WRAPPER, "", STRIP_ADMIT_TACTIC_WRAPPER)
                 for absolutize_mods in (False, True)
                 for first_wrap_then_include in ((True, False) if kwargs["prefer_inline_via_include"] else (False, True))
-                for without_require, insert_at_top in ((True, False), (False, True), (False, False))
+                for without_require, insert_at_top in ((True, False), (False, True), (False, False), (True, True))
                 for extra_top_header in (None, "Import Coq.Init.Prelude.")
                 for include_options_settings in (False, True)
             ]

Original file line number	Diff line number	Diff line change
`@@ -2719,7 +2719,7 @@ def get_test_output(`
`2719`	`2719`	`for admit_tactic_wrapper_action in (ADD_ADMIT_TACTIC_WRAPPER, "", STRIP_ADMIT_TACTIC_WRAPPER)`
`2720`	`2720`	`for absolutize_mods in (False, True)`
`2721`	`2721`	`for first_wrap_then_include in ((True, False) if kwargs["prefer_inline_via_include"] else (False, True))`
`2722`		`- for without_require, insert_at_top in ((True, False), (False, True), (False, False))`
	`2722`	`+ for without_require, insert_at_top in ((True, False), (False, True), (False, False), (True, True))`
`2723`	`2723`	`for extra_top_header in (None, "Import Coq.Init.Prelude.")`
`2724`	`2724`	`for include_options_settings in (False, True)`
`2725`	`2725`	`]`