7 files changed, 83 insertions, 15 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index d4ad438d61..59cc3e5a38 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -629,7 +629,14 @@ $(addsuffix .log,$(wildcard ideal-features/*.v)): %.v.log: %.v $(PREREQUISITELOG
 	} > "$@"
 
 # Additional dependencies for module tests
-$(addsuffix .log,$(wildcard modules/*.v)): %.v.log: modules/Nat.vo modules/plik.vo
+COMMON_MODULE_DEPENDENCIES := modules/plik.v modules/Nat.v
+# We exclude Nat.v.log and plik.v.log because these log files do not
+# depend on having the corresponding .vo files built first, and we end
+# up with pseudo-cyclic build rules if we don't exclude them (See
+# COQBUG(https://github.com/coq/coq/issues/12582)). Additionally, we
+# impose order-only dependencies to ensure that we won't rebuild the
+# .vo files in the .log target after we've already built them.
+$(addsuffix .log,$(filter-out $(COMMON_MODULE_DEPENDENCIES),$(wildcard modules/*.v))): %.v.log: $(COMMON_MODULE_DEPENDENCIES:.v=.vo) | $(COMMON_MODULE_DEPENDENCIES:.v=.v.log)
 modules/%.vo: modules/%.v
 	$(HIDE)$(coqc) -R modules Mods $<
 
diff --git a/test-suite/bugs/closed/bug_12228.v b/test-suite/bugs/closed/bug_12228.v
new file mode 100644
index 0000000000..a874fa0570
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12228.v
@@ -0,0 +1,4 @@
+Tactic Notation "mark" constr(P) "at" integer_list(L) := pattern P at L.
+Goal 0 = 0.
+mark 0 at -2.
+Abort.
diff --git a/test-suite/bugs/closed/bug_12532.v b/test-suite/bugs/closed/bug_12532.v
new file mode 100644
index 0000000000..665f6643e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12532.v
@@ -0,0 +1,56 @@
+(** This is a change of behaviour introduced by PR #12532. It is not clear
+    whether it is a legit behaviour but it is worth having it in the test
+    suite. *)
+
+Module Foo.
+
+Axiom whatever : Type.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo : forall st st', In st -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name), In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+solve [debug eauto].
+Abort.
+
+End Foo.
+
+Module Bar.
+
+Axiom whatever : Type.
+Axiom AppendEntries : whatever -> Prop.
+Axiom name : Type.
+Axiom nw : forall (P : Type), name -> P.
+Axiom raft_data : Type.
+Axiom In : raft_data -> Prop.
+
+Axiom foo :
+  forall st st' lid,
+    (AppendEntries lid -> In st) -> AppendEntries lid -> In st'.
+
+Definition params := prod whatever raft_data.
+
+Goal forall
+  (d : raft_data),
+  (forall (h : name) (w : whatever),
+    AppendEntries w -> In (@snd whatever raft_data (@nw params h))) ->
+  In d.
+Proof.
+intros.
+eapply foo.
+intros.
+solve [debug eauto].
+Abort.
+
+End Bar.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 04514c15cb..edd2c9674f 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -37,10 +37,10 @@ Arguments wrap {A}%type_scope {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-foo@{u UnivBinders.18 v} = 
-Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.18+1,v+1)}
-(* u UnivBinders.18 v |=  *)
+foo@{u u0 v} = 
+Type@{u0} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,u0+1,v+1)}
+(* u u0 v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -76,10 +76,10 @@ foo@{E M N} =
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u UnivBinders.18 v} = 
-Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.18+1,v+1)}
-(* u UnivBinders.18 v |=  *)
+foo@{u u0 v} = 
+Type@{u0} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,u0+1,v+1)}
+(* u u0 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
@@ -142,16 +142,14 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.58 UnivBinders.59} :
-Type@{UnivBinders.58} -> Type@{i}
-(* i UnivBinders.58 UnivBinders.59 |=  *)
+axfoo@{i u u0} : Type@{u} -> Type@{i}
+(* i u u0 |=  *)
 
 axfoo is universe polymorphic
 Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.58 UnivBinders.59} :
-Type@{UnivBinders.59} -> Type@{i}
-(* i UnivBinders.58 UnivBinders.59 |=  *)
+axbar@{i u u0} : Type@{u0} -> Type@{i}
+(* i u u0 |=  *)
 
 axbar is universe polymorphic
 Arguments axbar _%type_scope
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 66305dfefa..563651cfa5 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 Module applydestruct.
   Class Foo (A : Type) :=
     { bar : nat -> A;
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index 62a66daf7d..98e2917300 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 (* Wish #2154 by E. van der Weegen *)
 
 (* auto was not using f_equal-style lemmas with metavariables occurring
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index cea7d92c0b..9577d63f61 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,3 +1,4 @@
+(* coq-prog-args: ("-async-proofs" "off") *)
 Require Import Program.Tactics.
 Module Backtracking.
   Class A := { foo : nat }.