anchor.diff:         ( noshort,
           "max_fuel", 
           OneArg((fun x -> Int (int_of_string x)), 
  -                "non-negative integer"), 
  +                "[non-negative integer]"), 
           "Number of unrolling of recursive functions to try at most (default 8)");
         
          ( noshort,
           "max_ifuel", 
           OneArg((fun x -> Int (int_of_string x)), 
  -                "non-negative integer"), 
  +                "[non-negative integer]"), 
           "Number of unrolling of inductive datatypes to try at most (default 2)");
         
          ( noshort,
           "min_fuel", 
           OneArg((fun x -> Int (int_of_string x)), 
  -                "non-negative integer"), 
  +                "[non-negative integer]"), 
           "Minimum number of unrolling of recursive functions to try (default 1)");
         
          ( noshort,
  
positive.code:        ( noshort,
          "universes", 
          ZeroArgs (fun () -> Bool true), 
          "Use the (experimental) support for universes");
        
         ( noshort,
          "unthrottle_inductives", 
  
negative.code:        ( noshort,
          "use_eq_at_higher_order", 
          ZeroArgs (fun () -> Bool true), 
          "Use equality constraints when comparing higher-order types (Temporary)");
        
         ( noshort,
          "use_native_int", 
          ZeroArgs (fun () -> Bool true), 
          "Extract the 'int' type to platform-specific native int (You will need to link the generated code with the appropriate version of the prims library)");
        
         ( noshort,
          "verify_module", 
          OneArg (cons_verify_module,
                   "[module name]"), 
          "Name of the module to verify");
        
         ( noshort,
          "__temp_no_proj", 
           OneArg ((fun x -> List (x :: get___temp_no_proj() |> List.map String)), 
                    "[module name]"), 
          "Don't generate projectors for this module");
   
         ( 'v', 
  