Properly reflect in "configure --help" the default setting for the --enable/disable options.

configure.in

@@ -48,95 +48,95 @@ AC_INIT(src/)
 # verbosemake
 
 AC_ARG_ENABLE(verbose-make,
-    [  --enable-verbose-make   verbose makefile commands],,
+    AS_HELP_STRING([--enable-verbose-make], [verbose makefile recipes]),,
     enable_verbose_make=no)
 
 # LOCAL_CONF
 
 AC_ARG_ENABLE(local,
-    [  --enable-local          use Why3 in the build directory (no installation)],,
+    AS_HELP_STRING([--enable-local], [use Why3 in the build directory (no installation)]),,
     enable_local=no)
 
 # RELOCATABLE INSTALLATION
 
 AC_ARG_ENABLE(relocation,
-    [  --enable-relocation     allow for later relocation of Why3 installation],,
+    AS_HELP_STRING([--enable-relocation], [allow for later relocation of Why3 installation]),,
     enable_relocation=no)
 
 # NATIVE
 
 AC_ARG_ENABLE(native-code,
-    [  --enable-native-code    use the native-code compiler if available],,
+    AS_HELP_STRING([--disable-native-code], [use only the byte-code compiler]),,
     enable_native_code=yes)
 
 # Zarith
 
 AC_ARG_ENABLE(zarith,
-    [  --enable-zarith         use extra arbitrary-precision lib Zarith],,
+    AS_HELP_STRING([--disable-zarith], [use Nums instead of Zarith for computations]),,
     enable_zarith=yes)
 
 
 # IDE
 
 AC_ARG_ENABLE(ide,
-    [  --enable-ide            enable Why3 IDE],,
+    AS_HELP_STRING([--disable-ide], [do not build Why3 IDE]),,
     enable_ide=yes)
 
 # Bench
 
 AC_ARG_ENABLE(bench,
-    [  --enable-bench          enable Why3 benchmarking tool],,
+    AS_HELP_STRING([--disable-bench], [do not build Why3 benchmarking tool]),,
     enable_bench=yes)
 
 # Coq tactic and libraries
 
 AC_ARG_ENABLE(coq-tactic,
-    [  --enable-coq-tactic     enable Coq "why3" tactic],,
+    AS_HELP_STRING([--disable-coq-tactic], [do not build Coq "why3" tactic]),,
     enable_coq_tactic=yes)
 
 AC_ARG_ENABLE(coq-libs,
-    [  --enable-coq-libs       enable Coq realizations],,
+    AS_HELP_STRING([--disable-coq-libs], [do not build Coq realizations]),,
     enable_coq_libs=yes)
 
 # PVS libraries
 
 AC_ARG_ENABLE(pvs-libs,
-    [  --enable-pvs-libs       enable PVS realizations],,
+    AS_HELP_STRING([--disable-pvs-libs], [do not build PVS realizations]),,
     enable_pvs_libs=yes)
 
 # Isabelle libraries
 
 AC_ARG_ENABLE(isabelle-libs,
-    [  --enable-isabelle-libs       enable Isabelle realizations],,
+    AS_HELP_STRING([--disable-isabelle-libs], [do not build Isabelle realizations]),,
     enable_isabelle_libs=yes)
 
 # hypothesis selection
 
 AC_ARG_ENABLE(hypothesis-selection,
-    [  --enable-hypothesis-selection    enable hypothesis selection support],,
+    AS_HELP_STRING([--disable-hypothesis-selection], [do not support hypothesis selection]),,
     enable_hypothesis_selection=yes)
 
 # documentation
 
 AC_ARG_ENABLE(doc,
-    [  --enable-doc            build documentation],,
+    AS_HELP_STRING([--disable-doc], [do not build documentation]),,
     enable_doc=yes)
 
 AC_ARG_ENABLE(html-doc,
-    [  --enable-html-doc       build HTML documentation],,
+    AS_HELP_STRING([--enable-html-doc], [do not build HTML documentation]),,
     enable_html_doc=yes)
 
 # Experimental Jessie3 Frama-C plugin, disabled by default
 
 AC_ARG_ENABLE(frama-c,
-    [  --enable-frama-c        enable Frama-C plugin],,
+    AS_HELP_STRING([--enable-frama-c], [enable Frama-C plugin]),,
     [enable_frama_c=no
      reason_frama_c=" (disabled by default)"])
 
 # profiling
 
 AC_ARG_ENABLE(profiling,
-    [  --enable-profiling      enable profiling],,
+    AS_HELP_STRING([--enable-profiling], [enable profiling]),,
     enable_profiling=no)
 
 # either relocation or local, not both