anchor.diff:               else Util.print_string (Util.format3 "  --%s %s  %s\n" (Util.colorize_bold flag) (Util.colorize_bold argname) doc))
       specs
   
  -let mk_spec (o:opt'<option_val>) : opt = 
  +let mk_spec (o:opt'<option_val>) : opt =
       let ns, name, arg, desc = o in
  -    let arg = 
  -        match arg with 
  -        | ZeroArgs f -> 
  +    let arg =
  +        match arg with
  +        | ZeroArgs f ->
             let g () = set_option' (name, f()) in
             ZeroArgs g
   
  -        | OneArg (f, d) -> 
  +        | OneArg (f, d) ->
             let g x = set_option' (name, f x) in
             OneArg (g, d) in
       ns, name, arg, desc
   
  -let cons_verify_module s  = 
  +let cons_verify_module s  =
       List (String.lowercase s::get_verify_module() |> List.map String)
   
  -let add_verify_module s = 
  +let add_verify_module s =
       set_option "verify_module" (cons_verify_module s)
   
   let rec specs () : list<Getopt.opt> =
     let specs =
  -    [( noshort, 
  -       "admit_smt_queries", 
  -       OneArg ((fun s -> if s="true" then Bool true 
  -                         else if s="false" then Bool false 
  -                         else failwith("Invalid argument to --admit_smt_queries")), 
  +    [( noshort,
  +       "admit_smt_queries",
  +       OneArg ((fun s -> if s="true" then Bool true
  +                         else if s="false" then Bool false
  +                         else failwith("Invalid argument to --admit_smt_queries")),
                   "[true|false]"),
          "Admit SMT queries, unsafe! (default 'false')");
   
  -     ( noshort, 
  -       "cardinality",       
  -       OneArg ((fun x -> String (validate_cardinality x)), 
  +     ( noshort,
  +       "cardinality",
  +       OneArg ((fun x -> String (validate_cardinality x)),
                  "[off|warn|check]"),
          "Check cardinality constraints on inductive data types (default 'off')");
   
  -     ( noshort, 
  -       "codegen", 
  -        OneArg ((fun s -> String (parse_codegen s)), 
  +     ( noshort,
  +       "codegen",
  +        OneArg ((fun s -> String (parse_codegen s)),
                    "[OCaml|FSharp]"),
           "Generate code for execution");
   
  -     ( noshort, 
  -        "codegen-lib", 
  -        OneArg ((fun s -> List (s::get_codegen_lib() |> List.map String)), 
  +     ( noshort,
  +        "codegen-lib",
  +        OneArg ((fun s -> List (s::get_codegen_lib() |> List.map String)),
                    "[namespace]"),
           "External runtime library");
  -     
  -     ( noshort, 
  -        "debug", 
  +
  +     ( noshort,
  +        "debug",
           OneArg ((fun x -> List (x::get_debug() |> List.map String)),
                    "[module name]"),
           "Print lots of debugging information while checking module");
  -      
  -       ( noshort,
  -        "debug_level", 
  -        OneArg ((fun x -> List (x::get_debug_level() |> List.map String)), 
  +
  +       ( noshort,
  +        "debug_level",
  +        OneArg ((fun x -> List (x::get_debug_level() |> List.map String)),
                    "[Low|Medium|High|Extreme|...]"),
           "Control the verbosity of debugging info");
  -      
  -       ( noshort,
  -        "dep", 
  +
  +       ( noshort,
  +        "dep",
           OneArg ((fun x -> if x = "make" || x = "graph" then String x else failwith "invalid argument to 'dep'"),
                    "[make|graph]"),
           "Output the transitive closure of the dependency graph in a format suitable for the given tool");
  -      
  -       ( noshort,
  -        "detail_errors", 
  +
  +       ( noshort,
  +        "detail_errors",
           ZeroArgs (fun () -> Bool true),
            "Emit a detailed error report by asking the SMT solver many queries; will take longer; implies n_cores=1; requires --universes");
  -      
  +
          ( noshort,
           "dump_module",
           OneArg ((fun x -> (x::get_dump_module()) |> List.map String |> List),
                    "[module name]"),
           "");
  -      
  -       ( noshort,
  -        "eager_inference", 
  +
  +       ( noshort,
  +        "eager_inference",
           ZeroArgs (fun () -> Bool true),
           "Solve all type-inference constraints eagerly; more efficient but at the cost of generality");
  -      
  -       ( noshort,
  -        "explicit_deps", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "explicit_deps",
  +        ZeroArgs (fun () -> Bool true),
           "Do not find dependencies automatically, the user provides them on the command-line");
  -      
  -       ( noshort,
  -        "fs_typ_app", 
  -        ZeroArgs (fun () -> Bool true), 
  -        "Allow the use of t<t1, 
  -       ..., 
  +
  +       ( noshort,
  +        "fs_typ_app",
  +        ZeroArgs (fun () -> Bool true),
  +        "Allow the use of t<t1,
  +       ...,
          tn> syntax for type applications; brittle since it clashes with the integer less-than operator");
  -      
  -       ( noshort,
  -        "fsi", 
  +
  +       ( noshort,
  +        "fsi",
           ZeroArgs (fun () -> Bool true),
           "fsi flag; A flag to indicate if type checking a fsi in the interactive mode");
  -      
  -       ( noshort,
  -        "fstar_home", 
  +
  +       ( noshort,
  +        "fstar_home",
           OneArg (String,
                   "[dir]"),
           "Set the FSTAR_HOME variable to [dir]");
  -      
  +
          ( noshort,
           "hide_genident_nums",
  -        ZeroArgs(fun () -> Bool true), 
  +        ZeroArgs(fun () -> Bool true),
           "Don't print generated identifier numbers");
  -      
  +
          ( noshort,
           "hide_uvar_nums",
           ZeroArgs(fun () -> Bool true),
           "Don't print unification variable numbers");
  -      
  +
          ( noshort,
           "in",
  -        ZeroArgs (fun () -> Bool true), 
  +        ZeroArgs (fun () -> Bool true),
           "Interactive mode; reads input from stdin");
  -      
  +
          ( noshort,
           "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",
  -        OneArg((fun x -> Int (int_of_string x)), 
  -                "[non-negative integer]"), 
  +        OneArg((fun x -> Int (int_of_string x)),
  +                "[non-negative integer]"),
           "Number of unrolling of recursive functions to try initially (default 2)");
  -      
  +
          ( noshort,
           "initial_ifuel",
  -        OneArg((fun x -> Int (int_of_string x)), 
  -                "[non-negative integer]"), 
  +        OneArg((fun x -> Int (int_of_string x)),
  +                "[non-negative integer]"),
           "Number of unrolling of inductive datatypes to try at first (default 1)");
  -      
  +
          ( noshort,
           "inline_arith",
  -        ZeroArgs(fun () -> Bool true), 
  +        ZeroArgs(fun () -> Bool true),
           "Inline definitions of arithmetic functions in the SMT encoding");
  -      
  +
          ( noshort,
           "lax",
  -        ZeroArgs (fun () -> Bool true), //pretype := true; verify := false), 
  +        ZeroArgs (fun () -> Bool true), //pretype := true; verify := false),
           "Run the lax-type checker only (admit all verification conditions)");
  -      
  +
          ( noshort,
           "log_types",
  -        ZeroArgs (fun () -> Bool true), 
  +        ZeroArgs (fun () -> Bool true),
           "Print types computed for data/val/let-bindings");
  -      
  -       ( noshort,
  -        "log_queries", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "log_queries",
  +        ZeroArgs (fun () -> Bool true),
           "Log the Z3 queries in queries.smt2");
  -      
  -       ( noshort,
  -        "max_fuel", 
  -        OneArg((fun x -> Int (int_of_string x)), 
  -                "[non-negative integer]"), 
  +
  +       ( noshort,
  +        "max_fuel",
  +        OneArg((fun x -> Int (int_of_string x)),
  +                "[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]"), 
  +
  +       ( noshort,
  +        "max_ifuel",
  +        OneArg((fun x -> Int (int_of_string x)),
  +                "[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]"), 
  +
  +       ( noshort,
  +        "min_fuel",
  +        OneArg((fun x -> Int (int_of_string x)),
  +                "[non-negative integer]"),
           "Minimum number of unrolling of recursive functions to try (default 1)");
  -      
  -       ( noshort,
  -        "MLish", 
  -        ZeroArgs(fun () -> Bool true),//ml_ish := true; full_context_dependency := false), 
  +
  +       ( noshort,
  +        "MLish",
  +        ZeroArgs(fun () -> Bool true),//ml_ish := true; full_context_dependency := false),
           "Introduce unification variables that are only dependent on the type variables in the context");
  -      
  -       ( noshort,
  -        "n_cores", 
  -        OneArg ((fun x -> Int (int_of_string x)),//; detail_errors := false), 
  -                 "[positive integer]"), 
  +
  +       ( noshort,
  +        "n_cores",
  +        OneArg ((fun x -> Int (int_of_string x)),//; detail_errors := false),
  +                 "[positive integer]"),
           "Maximum number of cores to use for the solver (implies detail_errors = false) (default 1)");
  -      
  -       ( noshort,
  -        "no_default_includes", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "no_default_includes",
  +        ZeroArgs (fun () -> Bool true),
           "Ignore the default module search paths");
  -      
  -       ( noshort,
  -        "no_extract", 
  +
  +       ( noshort,
  +        "no_extract",
           OneArg ((fun x -> List (x :: get_no_extract() |> List.map String)),
  -                 "[module name]"), 
  +                 "[module name]"),
           "Do not extract code from this module");
  -      
  -       ( noshort,
  -        "no_location_info", 
  +
  +       ( noshort,
  +        "no_location_info",
           ZeroArgs (fun () -> Bool true),
           "Suppress location information in the generated OCaml output (only relevant with --codegen OCaml)");
  -      
  -       ( noshort,
  -        "odir", 
  +
  +       ( noshort,
  +        "odir",
           OneArg (String,
  -                "[dir]"), 
  +                "[dir]"),
           "Place output in directory [dir]");
  -      
  -       ( noshort,
  -        "prims", 
  -        OneArg (String, 
  -                "file"), 
  +
  +       ( noshort,
  +        "prims",
  +        OneArg (String,
  +                "file"),
           "");
  -      
  -       ( noshort,
  -        "print_before_norm", 
  -        ZeroArgs(fun () -> Bool true), // norm_then_print := false), 
  +
  +       ( noshort,
  +        "print_before_norm",
  +        ZeroArgs(fun () -> Bool true), // norm_then_print := false),
           "Do not normalize types before printing (for debugging)");
  -      
  -       ( noshort,
  -        "print_bound_var_types", 
  -        ZeroArgs(fun () -> Bool true), 
  +
  +       ( noshort,
  +        "print_bound_var_types",
  +        ZeroArgs(fun () -> Bool true),
           "Print the types of bound variables");
  -      
  -       ( noshort,
  -        "print_effect_args", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "print_effect_args",
  +        ZeroArgs (fun () -> Bool true),
           "Print inferred predicate transformers for all computation types");
  -      
  -       ( noshort,
  -        "print_fuels", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "print_fuels",
  +        ZeroArgs (fun () -> Bool true),
           "Print the fuel amounts used for each successful query");
  -      
  -       ( noshort,
  -        "print_implicits", 
  -        ZeroArgs(fun () -> Bool true), 
  +
  +       ( noshort,
  +        "print_implicits",
  +        ZeroArgs(fun () -> Bool true),
           "Print implicit arguments");
  -      
  -       ( noshort,
  -        "print_universes", 
  -        ZeroArgs(fun () -> Bool true), 
  +
  +       ( noshort,
  +        "print_universes",
  +        ZeroArgs(fun () -> Bool true),
           "Print universes");
  -      
  -       ( noshort,
  -        "prn", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "prn",
  +        ZeroArgs (fun () -> Bool true),
           "Print real names (you may want to use this in conjunction with log_queries)");
  -      
  -       ( noshort,
  -        "show_signatures", 
  -        OneArg((fun x -> List (x::get_show_signatures() |> List.map String)), 
  -                "[module name]"), 
  +
  +       ( noshort,
  +        "show_signatures",
  +        OneArg((fun x -> List (x::get_show_signatures() |> List.map String)),
  +                "[module name]"),
           "Show the checked signatures for all top-level symbols in the module");
  -      
  -       ( noshort,
  -        "silent", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "silent",
  +        ZeroArgs (fun () -> Bool true),
           " ");
  -      
  -       ( noshort,
  -        "smt", 
  -        OneArg (String, 
  -                 "[path]"), 
  -        "Path to the SMT solver (usually Z3, 
  +
  +       ( noshort,
  +        "smt",
  +        OneArg (String,
  +                 "[path]"),
  +        "Path to the SMT solver (usually Z3,
           but could be any SMT2-compatible solver)");
  -      
  -       ( noshort,
  -        "split_cases", 
  -        OneArg ((fun n -> Int (int_of_string n)), 
  -                 "[positive integer]"), 
  +
  +       ( noshort,
  +        "split_cases",
  +        OneArg ((fun n -> Int (int_of_string n)),
  +                 "[positive integer]"),
           "Partition VC of a match into groups of [n] cases");
  -      
  -       ( noshort,
  -        "timing", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "timing",
  +        ZeroArgs (fun () -> Bool true),
           "Print the time it takes to verify each top-level definition");
  -      
  -       ( noshort,
  -        "trace_error", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "trace_error",
  +        ZeroArgs (fun () -> Bool true),
           "Don't print an error message; show an exception trace instead");
  -      
  -       ( noshort,
  -        "universes", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "universes",
  +        ZeroArgs (fun () -> Bool true),
           "Use the support for universes");
  -      
  -       ( noshort,
  -        "unthrottle_inductives", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( noshort,
  +        "unthrottle_inductives",
  +        ZeroArgs (fun () -> Bool true),
           "Let the SMT solver unfold inductive types to arbitrary depths (may affect verifier performance)");
  -      
  -       ( noshort,
  -        "use_eq_at_higher_order", 
  -        ZeroArgs (fun () -> Bool true), 
  +
  +       ( 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), 
  +
  +       ( 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", 
  +
  +       ( noshort,
  +        "verify_module",
           OneArg (cons_verify_module,
  -                 "[module name]"), 
  +                 "[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]"), 
  +
  +       ( 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', 
  -         "version", 
  -         ZeroArgs (fun _ -> display_version(); exit 0), 
  +
  +       ( 'v',
  +         "version",
  +         ZeroArgs (fun _ -> display_version(); exit 0),
            "Display version number");
  -      
  -       ( noshort,
  -        "warn_top_level_effects", 
  -        ZeroArgs (fun () -> Bool true), 
  -        "Top-level effects are ignored, 
  +
  +       ( noshort,
  +        "warn_top_level_effects",
  +        ZeroArgs (fun () -> Bool true),
  +        "Top-level effects are ignored,
           by default; turn this flag on to be warned when this happens");
  -      
  -       ( noshort,
  -        "z3timeout", 
  -         OneArg ((fun s -> Int (int_of_string s)), 
  -                  "[positive integer]"), 
  +
  +       ( noshort,
  +        "z3timeout",
  +         OneArg ((fun s -> Int (int_of_string s)),
  +                  "[positive integer]"),
           "Set the Z3 per-query (soft) timeout to [t] seconds (default 5)");
     ] in
  -     ( 'h', 
  -        "help", 
  -        ZeroArgs (fun x -> display_usage_aux specs; exit 0), 
  +     ( 'h',
  +        "help",
  +        ZeroArgs (fun x -> display_usage_aux specs; exit 0),
           "Display this information")::List.map mk_spec specs
  -        
  +
   and parse_codegen s =
     match s with
     | "OCaml"
  
positive.code:     with _ ->
        None
  
  let prims () = 
    match get_prims() with
    | None ->
      let filen = "prims.fst" in
  
negative.code:         ("verify"                       , Bool true);
          ("verify_module"                , List []);
          ("warn_top_level_effects"       , Bool false);
          ("z3timeout"                    , Int 5)] in
     let o = peek () in
     Util.smap_clear o;
     vals |> List.iter set_option'                          //initialize it with the default values
  
  let clear () =
     let o = Util.smap_create 50 in
     fstar_options := [o];                                 //clear and reset the options stack
     init()
  
  let _run = clear()
  
  let lookup_opt s c =
    match Util.smap_try_find (peek()) s with
    | None -> failwith ("Impossible: option " ^s^ " not found")
    | Some s -> c s
  
  let get_admit_smt_queries       ()      = lookup_opt "admit_smt_queries"        as_bool
  let get_cardinality             ()      = lookup_opt "cardinality"              as_string
  let get_codegen                 ()      = lookup_opt "codegen"                  (as_option as_string)
  let get_codegen_lib             ()      = lookup_opt "codegen-lib"              (as_list as_string)
  let get_debug                   ()      = lookup_opt "debug"                    (as_list as_string)
  