[toplevel] Deprecate the `-compile` flag in favor of `coqc`.

This PR deprecates the use of `coqtop` as a compiler.

There is no point on having two binaries with the same purpose; after
the experiment in #8690, IMHO we have a lot to gain in terms of code
organization by splitting the compiler and the interactive binary.

We adapt the documentation and adapt the test-suite.

Note that we don't make `coqc` a true binary yet, but here we take
care only of the user-facing part.

The conversion of the binary will take place in #8690 and will bring
code simplification, including a unified handling of arguments.

8 files changed, 7 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 72d5a9253a..7a64b7eb45 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -50,4 +50,4 @@ myAnd1 True True
 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/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.