9 files changed, 27 insertions, 6 deletions
diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v
index 7658ce718e..440fe46003 100644
--- a/test-suite/output/FunExt.v
+++ b/test-suite/output/FunExt.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-async-proofs" "no") -*- *)
 Require Import FunctionalExtensionality.
 
 (* Basic example *)
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 94016e170b..7a64b7eb45 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -45,5 +45,9 @@ fun x : nat => (x.-1)%pred
      : Prop
 ##
      : Prop
+myAnd1 True True
+     : Prop
+r 2 3
+     : Prop
 Notation Cn := Foo.FooCn
-Expands to: Notation Top.J.Mfoo.Foo.Bar.Cn
+Expands to: Notation Notations4.J.Mfoo.Foo.Bar.Cn
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 309115848f..90babf9c55 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -165,6 +165,22 @@ Check ##.
 
 End H.
 
+(* Fixing bugs reported by G. Gonthier in #9207 *)
+
+Module I.
+
+Definition myAnd A B := A /\ B.
+Notation myAnd1 A := (myAnd A).
+Check myAnd1 True True.
+
+Set Warnings "-auto-template".
+
+Record Pnat := {inPnat :> nat -> Prop}.
+Axiom r : nat -> Pnat.
+Check r 2 3.
+
+End I.
+
 (* Fixing a bug reported by G. Gonthier in #9207 *)
 
 Module J.
diff --git a/test-suite/output/RecognizePluginWarning.v b/test-suite/output/RecognizePluginWarning.v
index cd667bbd00..a53b52396f 100644
--- a/test-suite/output/RecognizePluginWarning.v
+++ b/test-suite/output/RecognizePluginWarning.v
@@ -1,4 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "extraction-logical-axiom") -*- *)
+(* -*- mode: coq; coq-prog-args: ("-w" "extraction-logical-axiom") -*- *)
 
 (* Test that mentioning a warning defined in plugins works. The failure
 mode here is that these result in a warning about unknown warnings, since the
diff --git a/test-suite/output/Show.v b/test-suite/output/Show.v
index 60faac8dd9..c875051bdc 100644
--- a/test-suite/output/Show.v
+++ b/test-suite/output/Show.v
@@ -5,7 +5,7 @@
 Theorem nums : forall (n m : nat), n = m -> (S n) = (S m).
 Proof.
   intros.
-  induction n as [| n'].  
+  induction n as [| n'].
   induction m as [| m'].
   Show.
 Admitted.
diff --git a/test-suite/output/UnclosedBlocks.v b/test-suite/output/UnclosedBlocks.v
index 854bd6a6d5..b9ba579246 100644
--- a/test-suite/output/UnclosedBlocks.v
+++ b/test-suite/output/UnclosedBlocks.v
@@ -1,4 +1,3 @@
-(* -*- mode: coq; coq-prog-args: ("-compile" "UnclosedBlocks.v") *)
 Module Foo.
   Module Closed.
   End Closed.
diff --git a/test-suite/output/UsePluginWarning.v b/test-suite/output/UsePluginWarning.v
index c6e0054641..618b8fd42f 100644
--- a/test-suite/output/UsePluginWarning.v
+++ b/test-suite/output/UsePluginWarning.v
@@ -1,5 +1,4 @@
-(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-extraction-logical-axiom") -*- *)
-
+(* -*- mode: coq; coq-prog-args: ("-w" "-extraction-logical-axiom") -*- *)
 Require Extraction.
 Axiom foo : Prop.
 
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 5f1926f142..5f7e3ab9dd 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -11,3 +11,4 @@ Undo.
 simpl (0 + _).
 Show.
 Undo.
+Abort.
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index 179dec3fb0..c987d66c5f 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -1,3 +1,4 @@
+(* -*- coq-prog-args: ("-async-proofs" "no") -*- *)
 (* Set Printing Existential Instances. *)
 Unset Solve Unification Constraints.
 Axiom veeryyyyyyyyyyyyloooooooooooooonggidentifier : nat.