From e7b25d6d37b7d3a925096aeb803562ece474c090 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 21 Sep 2017 14:36:15 +0200
Subject: Remove remaining occurrences of -just-parsing.

---
 tools/coqc.ml      | 2 +-
 toplevel/coqtop.ml | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 862225d3d1..b381c5ba42 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -93,7 +93,7 @@ let parse_args () =
 
     | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
-      |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
+      |"-q"|"-profile"|"-echo" |"-quiet"
       |"-silent"|"-m"|"-beautify"|"-strict-implicit"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 0f8524e923..1f75e166b4 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -565,7 +565,6 @@ let parse_args arglist =
     |"-ideslave" -> set_ideslave ()
     |"-impredicative-set" -> set_impredicative_set ()
     |"-indices-matter" -> Indtypes.enforce_indices_matter ()
-    |"-just-parsing" -> warning "-just-parsing option has been removed in 8.6"
     |"-m"|"--memory" -> memory_stat := true
     |"-noinit"|"-nois" -> load_init := false
     |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
-- 
cgit v1.2.3