diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-12 22:12:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-08-01 18:42:44 +0200 |
| commit | 2def58217686b5083da38778a5ebffb451b1d4d6 (patch) | |
| tree | c0c2463a4620fe3c6bb2caf21a70f6861bbb4643 /tools/coqc.ml | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
[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.
Diffstat (limited to 'tools/coqc.ml')
| -rw-r--r-- | tools/coqc.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index 4595af6e8..862225d3d 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" |