diff options
| author | Maxime Dénès | 2017-08-29 14:34:17 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-08-29 14:34:17 +0200 |
| commit | 75d70664156bf1715b4eb9933a684a344f43467d (patch) | |
| tree | 0f98f6fb7b1d39e8aae86c45ba7b2e36b3a91f53 /tools | |
| parent | 0c566066f92728d9a848e1f60f52dd09c1a727f2 (diff) | |
| parent | 2def58217686b5083da38778a5ebffb451b1d4d6 (diff) | |
Merge PR #773: [flags] Remove XML output flag.
Diffstat (limited to 'tools')
| -rwxr-xr-x | tools/beautify-archive | 2 | ||||
| -rwxr-xr-x | tools/check-translate | 2 | ||||
| -rw-r--r-- | tools/coqc.ml | 2 |
3 files changed, 3 insertions, 3 deletions
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" |