anchor.diff:         ( noshort,
           "fstar_home", 
           OneArg (String,
  -                "dir"), 
  -        "Set the FSTAR_HOME variable to dir");
  -      
  -       ( noshort,
  -        "hide_genident_nums", 
  +                "[dir]"),
  +        "Set the FSTAR_HOME variable to [dir]");
  +      
  +       ( noshort,
  +        "hide_genident_nums",
           ZeroArgs(fun () -> Bool true), 
           "Don't print generated identifier numbers");
         
          ( noshort,
  -        "hide_uvar_nums", 
  +        "hide_uvar_nums",
           ZeroArgs(fun () -> Bool true),
           "Don't print unification variable numbers");
         
          ( noshort,
  -        "in", 
  +        "in",
           ZeroArgs (fun () -> Bool true), 
           "Interactive mode; reads input from stdin");
         
          ( noshort,
  -        "include", 
  +        "include",
           OneArg ((fun s -> List (get_include() @ [s] |> List.map String)),
  -                "path"), 
  +                "[path]"), 
           "A directory in which to search for files included on the command line");
         
          ( noshort,
  -        "initial_fuel", 
  +        "initial_fuel",
           OneArg((fun x -> Int (int_of_string x)), 
  -                "non-negative integer"), 
  +                "[non-negative integer]"), 
           "Number of unrolling of recursive functions to try initially (default 2)");
         
          ( noshort,
  -        "initial_ifuel", 
  +        "initial_ifuel",
           OneArg((fun x -> Int (int_of_string x)), 
  -                "non-negative integer"), 
  +                "[non-negative integer]"), 
           "Number of unrolling of inductive datatypes to try at first (default 1)");
         
          ( noshort,
  -        "inline_arith", 
  +        "inline_arith",
           ZeroArgs(fun () -> Bool true), 
           "Inline definitions of arithmetic functions in the SMT encoding");
         
          ( noshort,
  -        "lax", 
  +        "lax",
           ZeroArgs (fun () -> Bool true), //pretype := true; verify := false), 
           "Run the lax-type checker only (admit all verification conditions)");
         
          ( noshort,
  -        "log_types", 
  +        "log_types",
           ZeroArgs (fun () -> Bool true), 
           "Print types computed for data/val/let-bindings");
         
  
positive.code:        ( noshort,
          "universes", 
          ZeroArgs (fun () -> Bool true), 
          "Use the (experimental) support for universes");
        
         ( noshort,
          "unthrottle_inductives", 
  
negative.code:        ( noshort,
          "explicit_deps", 
          ZeroArgs (fun () -> Bool true), 
          "Do not find dependencies automatically, the user provides them on the command-line");
        
         ( noshort,
          "fs_typ_app", 
  