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 /toplevel/usage.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 'toplevel/usage.ml')
| -rw-r--r-- | toplevel/usage.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 962bb4302..d596e36f3 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -78,9 +78,6 @@ let print_usage_channel co command = \n -impredicative-set set sort Set impredicative\ \n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\ \n -type-in-type disable universe consistency checking\ -\n -xml export XML files either to the hierarchy rooted in\ -\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ -\n stdout (if unset)\ \n -time display the time taken by each command\ \n -profile-ltac display the time taken by each (sub)tactic\ \n -m, --memory display total heap size at program exit\ |