diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index a2c1cabb23..2984be95e8 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -174,6 +174,7 @@ tactics (see Chapters ring and micromega), there are also:
     From Stdlib Require Import DiscrR.
     Open Scope R_scope.
     Goal 5 <> 0.
+    Proof.
     discrR.
 
 .. tacn:: split_Rabs
@@ -187,6 +188,7 @@ tactics (see Chapters ring and micromega), there are also:
     From Stdlib Require Import Reals.
     Open Scope R_scope.
     Goal forall x:R, x <= Rabs x.
+    Proof.
     intro; split_Rabs.
 
 .. tacn:: split_Rmult
@@ -201,6 +203,7 @@ tactics (see Chapters ring and micromega), there are also:
     From Stdlib Require Import Reals.
     Open Scope R_scope.
     Goal forall x y z:R, x * y * z <> 0.
+    Proof.
     intros; split_Rmult.
 
 List library
diff --git a/test-suite/output/BinaryPrintingNotations.v b/test-suite/output/BinaryPrintingNotations.v
index 783dd00813..b5cb318b70 100644
Binary files a/test-suite/output/BinaryPrintingNotations.v and b/test-suite/output/BinaryPrintingNotations.v differ
diff --git a/test-suite/output/FunExt.v b/test-suite/output/FunExt.v
index f1b0f63b5f..bbc09ea257 100644
--- a/test-suite/output/FunExt.v
+++ b/test-suite/output/FunExt.v
@@ -3,6 +3,7 @@ From Stdlib Require Import FunctionalExtensionality.
 
 (* Basic example *)
 Goal (forall x y z, x+y+z = z+y+x) -> (fun x y z => z+y+x) = (fun x y z => x+y+z).
+Proof.
 intro H.
 extensionality in H.
 symmetry in H.
@@ -11,6 +12,7 @@ Qed.
 
 (* Test rejection of non-equality *)
 Goal forall H:(forall A:Prop, A), H=H -> forall H'':True, H''=H''.
+Proof.
 intros H H' H''.
 Fail extensionality in H.
 clear H'.
@@ -20,6 +22,7 @@ Abort.
 
 (* Test success on dependent equality *)
 Goal forall (p : forall x, S x = x + 1), p = p -> S = fun x => x + 1.
+Proof.
 intros p H.
 extensionality in p.
 assumption.
@@ -28,6 +31,7 @@ Qed.
 (* Test dependent functional extensionality *)
 Goal forall (P:nat->Type) (Q:forall a, P a -> Type) (f g:forall a (b:P a), Q a b),
    (forall x y, f x y = g x y) -> f = g.
+Proof.
 intros * H.
 extensionality in H.
 assumption.
diff --git a/test-suite/output/Intuition.v b/test-suite/output/Intuition.v
index b42a021b99..c338d1f69a 100644
--- a/test-suite/output/Intuition.v
+++ b/test-suite/output/Intuition.v
@@ -1,5 +1,6 @@
 From Stdlib Require Import BinInt.
 Goal forall m n : Z, (m >= n)%Z -> (m >= m)%Z /\ (m >= n)%Z.
+Proof.
 intros; intuition.
 Show.
 Abort.
diff --git a/test-suite/output/RealNumberSyntax.v b/test-suite/output/RealNumberSyntax.v
index dd009ae6aa..afc36cc3cf 100644
--- a/test-suite/output/RealNumberSyntax.v
+++ b/test-suite/output/RealNumberSyntax.v
@@ -54,11 +54,13 @@ Close Scope hex_R_scope.
 From Stdlib Require Import Reals.
 
 Goal 254e3 = 2540 * 10 ^ 2.
+Proof.
 ring.
 Qed.
 
 From Stdlib Require Import Psatz.
 
 Goal 254e3 = 2540 * 10 ^ 2.
+Proof.
 lra.
 Qed.
diff --git a/test-suite/output/allBytes.v b/test-suite/output/allBytes.v
index 557250f5de..830217e309 100644
--- a/test-suite/output/allBytes.v
+++ b/test-suite/output/allBytes.v
@@ -120,5 +120,6 @@ Notation "'~'" := (Byte.x7e) (only printing, at level 0).
 Set Printing Depth 100.
 
 Goal False.
+Proof.
   let cc := eval cbv in allBytes in idtac cc.
 Abort.
diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index dec69efe93..e6fa3334da 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -1,6 +1,7 @@
 (* Simpl with patterns *)
 
 Goal forall x, 0+x = 1+x.
+Proof.
 intro x.
 simpl (_ + x).
 Show.
@@ -182,13 +183,13 @@ Check "DirectTuple (PrimitiveProjectionUnfolded)".
 Record T := {p:nat}.
 Definition a := {|p:=0|}.
 Axiom P : nat -> Prop.
-Goal P a.(p). unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
-Goal P a.(p). unfold p. cbv delta [a]. cbn. Show. Abort.   (* -> 0 *)
-Goal P a.(p). unfold p. cbv delta [a]. hnf. Show. Abort.   (* -> 0 *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. cbn. Show. Abort.   (* -> 0 *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. hnf. Show. Abort.   (* -> 0 *)
 Arguments p : simpl never.
-Goal P a.(p). unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
-Goal P a.(p). unfold p. cbv delta [a]. cbn. Show. Abort.   (* -> {| p := 0 |}.(p) *)
-Goal P a.(p). unfold p. cbv delta [a]. hnf. Show. Abort.   (* -> 0 *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. simpl. Show. Abort. (* -> 0 *) (* bug never 3 *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. cbn. Show. Abort.   (* -> {| p := 0 |}.(p) *)
+Goal P a.(p). Proof. unfold p. cbv delta [a]. hnf. Show. Abort.   (* -> 0 *)
 End DirectTuple.
 
 Module NamedTuple.
@@ -196,18 +197,18 @@ Check "NamedTuple (PrimitiveProjectionUnfolded)".
 Record T := {p:nat}.
 Definition a := {|p:=0|}.
 Axiom P : nat -> Prop.
-Goal P a.(p). unfold p. simpl. Show. Abort. (* -> 0 *)
-Goal P a.(p). unfold p. cbn. Show. Abort.   (* -> 0 *)
-Goal P a.(p). unfold p. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
+Goal P a.(p). Proof. unfold p. simpl. Show. Abort. (* -> 0 *)
+Goal P a.(p). Proof. unfold p. cbn. Show. Abort.   (* -> 0 *)
+Goal P a.(p). Proof. unfold p. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
 Arguments p : simpl never.
-Goal P a.(p). unfold p. simpl. Show. Abort. (* -> 0 *)     (* bug never 3 *)
-Goal P a.(p). unfold p. cbn. Show. Abort.   (* -> a.(p) *)
-Goal P a.(p). unfold p. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
+Goal P a.(p). Proof. unfold p. simpl. Show. Abort. (* -> 0 *)     (* bug never 3 *)
+Goal P a.(p). Proof. unfold p. cbn. Show. Abort.   (* -> a.(p) *)
+Goal P a.(p). Proof. unfold p. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
 Arguments p : simpl nomatch.
 Arguments a : simpl never.
-Goal P a.(p). unfold p. simpl. Show. Abort.  (* -> 0 *)     (* bug never 1 *)
-Goal P a.(p). unfold p. cbn. Show. Abort.    (* -> a.(p) *)
-Goal P a.(p). unfold p. hnf. Show. Abort.    (* -> a.(p) *) (* bug primproj 2 *)
+Goal P a.(p). Proof. unfold p. simpl. Show. Abort.  (* -> 0 *)     (* bug never 1 *)
+Goal P a.(p). Proof. unfold p. cbn. Show. Abort.    (* -> a.(p) *)
+Goal P a.(p). Proof. unfold p. hnf. Show. Abort.    (* -> a.(p) *) (* bug primproj 2 *)
 End NamedTuple.
 
 Module DirectCoFix.
@@ -216,13 +217,13 @@ CoInductive U := {q:U}.
 CoFixpoint a := {|q:=a|}.
 Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
-Goal P a.(q). unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *)
-Goal P a.(q). unfold q. cbv delta [a]. cbn. Show. Abort.   (* -> COFIX *)
-Goal P a.(q). unfold q. cbv delta [a]. hnf. Show. Abort.   (* -> COFIX *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. cbn. Show. Abort.   (* -> COFIX *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. hnf. Show. Abort.   (* -> COFIX *)
 Arguments q : simpl never.
-Goal P a.(q). unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *) (* never not respected on purpose *)
-Goal P a.(q). unfold q. cbv delta [a]. cbn. Show. Abort.   (* -> COFIX.(q) *)
-Goal P a.(q). unfold q. cbv delta [a]. hnf. Show. Abort.   (* -> COFIX *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. simpl. Show. Abort. (* -> COFIX *) (* never not respected on purpose *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. cbn. Show. Abort.   (* -> COFIX.(q) *)
+Goal P a.(q). Proof. unfold q. cbv delta [a]. hnf. Show. Abort.   (* -> COFIX *)
 End DirectCoFix.
 
 Module NamedCoFix.
@@ -231,18 +232,18 @@ CoInductive U := {q:U}.
 CoFixpoint a := {|q:=a|}.
 Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
-Goal P a.(q). unfold q. simpl. Show. Abort.  (* -> a *)
-Goal P a.(q). unfold q. cbn. Show. Abort.    (* -> a *)
-Goal P a.(q). unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P a.(q). Proof. unfold q. simpl. Show. Abort.  (* -> a *)
+Goal P a.(q). Proof. unfold q. cbn. Show. Abort.    (* -> a *)
+Goal P a.(q). Proof. unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 Arguments q : simpl never.
-Goal P a.(q). unfold q. simpl. Show. Abort.  (* -> a *)
-Goal P a.(q). unfold q. cbn. Show. Abort.    (* -> a.(q) *)
-Goal P a.(q). unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P a.(q). Proof. unfold q. simpl. Show. Abort.  (* -> a *)
+Goal P a.(q). Proof. unfold q. cbn. Show. Abort.    (* -> a.(q) *)
+Goal P a.(q). Proof. unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 Arguments q : simpl nomatch.
 Arguments a : simpl never.
-Goal P a.(q). unfold q. simpl. Show. Abort.  (* -> a *)
-Goal P a.(q). unfold q. cbn. Show. Abort.    (* -> a.(q) *)
-Goal P a.(q). unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P a.(q). Proof. unfold q. simpl. Show. Abort.  (* -> a *)
+Goal P a.(q). Proof. unfold q. cbn. Show. Abort.    (* -> a.(q) *)
+Goal P a.(q). Proof. unfold q. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 End NamedCoFix.
 End PrimitiveProjectionUnfolded.
 
@@ -257,13 +258,13 @@ Record T := {p:nat}.
 Abbreviation TUPLE := {|p:=0|}.
 Definition a := {|p:=0|}.
 Axiom P : nat -> Prop.
-Goal P (id p a). unfold id. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
-Goal P (id p a). unfold id. cbv delta [a]. cbn. Show. Abort.   (* -> 0 *)
-Goal P (id p a). unfold id. cbv delta [a]. hnf. Show. Abort.   (* -> TUPLE.(p) *) (* bug primproj 1 *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. simpl. Show. Abort. (* -> 0 *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. cbn. Show. Abort.   (* -> 0 *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. hnf. Show. Abort.   (* -> TUPLE.(p) *) (* bug primproj 1 *)
 Arguments p : simpl never.
-Goal P (id p a). unfold id. cbv delta [a]. simpl. Show. Abort. (* -> TUPLE.(p) *)
-Goal P (id p a). unfold id. cbv delta [a]. cbn. Show. Abort.   (* -> TUPLE.(p) *)
-Goal P (id p a). unfold id. cbv delta [a]. hnf. Show. Abort.   (* -> TUPLE.(p) *) (* bug primproj 1 *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. simpl. Show. Abort. (* -> TUPLE.(p) *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. cbn. Show. Abort.   (* -> TUPLE.(p) *)
+Goal P (id p a). Proof. unfold id. cbv delta [a]. hnf. Show. Abort.   (* -> TUPLE.(p) *) (* bug primproj 1 *)
 End DirectTuple.
 
 Module NamedTuple.
@@ -271,18 +272,18 @@ Check "NamedTuple (PrimitiveProjectionConstant)".
 Record T := {p:nat}.
 Definition a := {|p:=0|}.
 Axiom P : nat -> Prop.
-Goal P (id p a). unfold id. simpl. Show. Abort. (* -> 0 *)
-Goal P (id p a). unfold id. cbn. Show. Abort.   (* -> 0 *)
-Goal P (id p a). unfold id. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
+Goal P (id p a). Proof. unfold id. simpl. Show. Abort. (* -> 0 *)
+Goal P (id p a). Proof. unfold id. cbn. Show. Abort.   (* -> 0 *)
+Goal P (id p a). Proof. unfold id. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
 Arguments p : simpl never.
-Goal P (id p a). unfold id. simpl. Show. Abort. (* -> a.(p) *)
-Goal P (id p a). unfold id. cbn. Show. Abort.   (* -> a.(p) *)
-Goal P (id p a). unfold id. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
+Goal P (id p a). Proof. unfold id. simpl. Show. Abort. (* -> a.(p) *)
+Goal P (id p a). Proof. unfold id. cbn. Show. Abort.   (* -> a.(p) *)
+Goal P (id p a). Proof. unfold id. hnf. Show. Abort.   (* -> a.(p) *) (* bug primproj 2 *)
 Arguments p : simpl nomatch.
 Arguments a : simpl never.
-Goal P (id p a). unfold id. simpl. Show. Abort.  (* -> 0 *) (* never not respected on purpose *)
-Goal P (id p a). unfold id. cbn. Show. Abort.    (* -> a.(p) *)
-Goal P (id p a). unfold id. hnf. Show. Abort.    (* -> a.(p) *)
+Goal P (id p a). Proof. unfold id. simpl. Show. Abort.  (* -> 0 *) (* never not respected on purpose *)
+Goal P (id p a). Proof. unfold id. cbn. Show. Abort.    (* -> a.(p) *)
+Goal P (id p a). Proof. unfold id. hnf. Show. Abort.    (* -> a.(p) *)
 End NamedTuple.
 
 Module DirectCoFix.
@@ -290,13 +291,13 @@ Check "DirectCoFix (PrimitiveProjectionConstant)".
 CoInductive U := {q:U}.
 Abbreviation COFIX := (cofix a := {|q:=a|}).
 Axiom P : U -> Prop.
-Goal P (id q COFIX). unfold id. simpl. Show. Abort.  (* -> COFIX *)
-Goal P (id q COFIX). unfold id. cbn. Show. Abort.    (* -> COFIX *)
-Goal P (id q COFIX). unfold id. hnf. Show. Abort.    (* -> COFIX.(q) *) (* bug primproj 3 *)
+Goal P (id q COFIX). Proof. unfold id. simpl. Show. Abort.  (* -> COFIX *)
+Goal P (id q COFIX). Proof. unfold id. cbn. Show. Abort.    (* -> COFIX *)
+Goal P (id q COFIX). Proof. unfold id. hnf. Show. Abort.    (* -> COFIX.(q) *) (* bug primproj 3 *)
 Arguments q : simpl never.
-Goal P (id q COFIX). unfold id. simpl. Show. Abort.  (* -> COFIX.(q) *)
-Goal P (id q COFIX). unfold id. cbn. Show. Abort.    (* -> COFIX.(q) *)
-Goal P (id q COFIX). unfold id. hnf. Show. Abort.    (* -> COFIX.(q) *) (* bug primproj 3 *)
+Goal P (id q COFIX). Proof. unfold id. simpl. Show. Abort.  (* -> COFIX.(q) *)
+Goal P (id q COFIX). Proof. unfold id. cbn. Show. Abort.    (* -> COFIX.(q) *)
+Goal P (id q COFIX). Proof. unfold id. hnf. Show. Abort.    (* -> COFIX.(q) *) (* bug primproj 3 *)
 End DirectCoFix.
 
 Module NamedCoFix.
@@ -304,17 +305,17 @@ Check "NamedCoFix (PrimitiveProjectionConstant)".
 CoInductive U := {q:U}.
 CoFixpoint a := {|q:=a|}.
 Axiom P : U -> Prop.
-Goal P (id q a). unfold id. simpl. Show. Abort.  (* -> a *)
-Goal P (id q a). unfold id. cbn. Show. Abort.    (* -> a *)
-Goal P (id q a). unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P (id q a). Proof. unfold id. simpl. Show. Abort.  (* -> a *)
+Goal P (id q a). Proof. unfold id. cbn. Show. Abort.    (* -> a *)
+Goal P (id q a). Proof. unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 Arguments q : simpl never.
-Goal P (id q a). unfold id. simpl. Show. Abort.  (* -> a.(q) *)
-Goal P (id q a). unfold id. cbn. Show. Abort.    (* -> a.(q) *)
-Goal P (id q a). unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P (id q a). Proof. unfold id. simpl. Show. Abort.  (* -> a.(q) *)
+Goal P (id q a). Proof. unfold id. cbn. Show. Abort.    (* -> a.(q) *)
+Goal P (id q a). Proof. unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 Arguments q : simpl nomatch.
 Arguments a : simpl never.
-Goal P (id q a). unfold id. simpl. Show. Abort.  (* -> a *) (* never not respected on purpose *)
-Goal P (id q a). unfold id. cbn. Show. Abort.    (* -> a.(q) *)
-Goal P (id q a). unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
+Goal P (id q a). Proof. unfold id. simpl. Show. Abort.  (* -> a *) (* never not respected on purpose *)
+Goal P (id q a). Proof. unfold id. cbn. Show. Abort.    (* -> a.(q) *)
+Goal P (id q a). Proof. unfold id. hnf. Show. Abort.    (* -> a.(q) *) (* bug primproj 4 *)
 End NamedCoFix.
 End PrimitiveProjectionConstant.
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index e7d78ac6ee..1ac8a5f931 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -1934,14 +1934,12 @@ Qed.
 
 Lemma Zsgn_19 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 < x + y)%Z.
 Proof.
- Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_12; assumption).
 Qed.
 
 Lemma Zsgn_20 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x + y < 0)%Z.
 Proof.
- Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_11; assumption).
 Qed.
@@ -1955,7 +1953,6 @@ Qed.
 
 Lemma Zsgn_22 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x <= 0)%Z.
 Proof.
- Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index f71178c581..0ccc29ddc4 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -284,8 +284,7 @@ Lemma Thales: forall O A B C D:point,
   (distance2 O B * distance2 O C = distance2 O D * distance2 O A
   /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
  \/ collinear O A B.
-geo_begin.
-Proof.
+Proof. geo_begin.
   idtac "Thales 2 goals".
   Time nsatz.
   Time nsatz.