From d9fb8db86d5b4ddc79a207c5f0ac32eb98215e78 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 29 Jan 2019 00:44:34 +0100
Subject: [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.
---
 dev/doc/profiling.txt | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'dev')

diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt
index 29e87df6b8..8455d13377 100644
--- a/dev/doc/profiling.txt
+++ b/dev/doc/profiling.txt
@@ -10,7 +10,7 @@ In Coq source folder:
 opam switch 4.05.0+trunk+fp
 ./configure -local -debug
 make
-perf record -g bin/coqtop -compile file.v
+perf record -g bin/coqc file.v
 perf report -g fractal,callee --no-children
 
 To profile only part of a file, first load it using
@@ -96,7 +96,7 @@ https://github.com/mshinwell/opam-repo-dev
 
 ### For memory dump:
 
-CAMLRUNPARAM=T,mj bin/coqtop -compile file.v
+CAMLRUNPARAM=T,mj bin/coqc file.v
 
 In another terminal:
 
@@ -112,7 +112,7 @@ number of objects and third is the place where the objects where allocated.
 
 ### For complete memory graph:
 
-CAMLRUNPARAM=T,gr bin/coqtop -compile file.v
+CAMLRUNPARAM=T,gr bin/coqc file.v
 
 In another terminal:
 
-- 
cgit v1.2.3