From 2def58217686b5083da38778a5ebffb451b1d4d6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 12 Jun 2017 22:12:02 +0200
Subject: [flags] Remove XML output flag.

This is a second try at removing the hooks for the legacy xml export
system which can't currently be tested.

It is also not included in the API, so it should either be included in
it or this PR be applied.
---
 tools/beautify-archive | 2 +-
 tools/check-translate  | 2 +-
 tools/coqc.ml          | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tools')

diff --git a/tools/beautify-archive b/tools/beautify-archive
index 6bfa974a53..a327ea44e1 100755
--- a/tools/beautify-archive
+++ b/tools/beautify-archive
@@ -23,7 +23,7 @@ cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
 cd $NEWARCHIVE
 rm description || true
 make clean
-make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS)' || \
  { echo ---- Failed to beautify; exit 1; }
 echo -------- Upgrading files in the beautification directory --------------
 beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
diff --git a/tools/check-translate b/tools/check-translate
index 3dd8240532..acb6f45903 100755
--- a/tools/check-translate
+++ b/tools/check-translate
@@ -2,7 +2,7 @@
 
 echo -------------- Producing translated files ---------------------
 rm */*/*.v8 >& /dev/null
-make COQ_XML=-translate theories || { echo ---- Failed to translate; exit 1; }
+make COQOPTS=-translate theories || { echo ---- Failed to translate; exit 1; }
 if [ -e translated ]; then rm -r translated; fi
 if [ -e successful-translation ]; then rm -r successful-translation; fi
 if [ -e failed-translation ]; then rm -r failed-translation; fi
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 4595af6e88..862225d3d1 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -94,7 +94,7 @@ let parse_args () =
     | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
-      |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit"
+      |"-silent"|"-m"|"-beautify"|"-strict-implicit"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
-- 
cgit v1.2.3