Exclude most of the modules for experimentation
Write some functions manipulating Choice for conversion purpose
Eliminate exceptions until bool module

Remarks:
- Exceptions are preserved via Choice2Of2
- Some functions are current shadowed for easy conversion
- Some exceptions originating from lib module are currently skipped
Revise Choice functions to follow ExtCore's conventions
Convert until tactics module

Mostly we lift from term0 to term and goalstate0 to goalstate.
Other lifting will be done on demand.
Now the core is compiling
Get all modules to compile
Define Choice.tryFind to catch leaking exceptions
Reorganized ExtCore- and FSharp.Compatibility.OCaml-related functions so it's easier to see what should (and will) be moved into those libraries, and what is NHol-specific.
Added the [<Experimental>] attribute to Ratio.normalize_ratio so we know where it's being used (because it doesn't actually do anything at the moment, and so could be the source of some errors).
Added some OPTIMIZE comments for later.
Modified the 'assoc' and 'rev_assoc' functions so they return an option value instead of raising an exception on failure.
Modified any code consuming 'assoc' and 'rev_assoc' to either remove the now-unneeded try/with, or pass the result through the new Option.getOrFailWith function which fails with the same message as 'assoc' and 'rev_assoc' would have.
Modified any places where an exception is caught then failwith is called so the caught exception is included as the InnerException when raising the new failure exception. This provides more informative stack traces, since the information in the original exception (i.e., where the actual problem occured) is retained.
Change some functions to use Choice instead of raising exceptions; modified call sites for those functions to pass the result through Choice.get to approximate the original behavior.
Commented out the 'can' function (in lib.fs) and "inlined" all uses of it; this makes it easier to remove uses of 'can' one-by-one, and also to keep track of where it's used (because it can result in some hard-to-find bugs).
Remove type_of and insert Choice.get at all call sites

These Choice.get calls should be removed later.
Remove exceptions from mk_type and mk_const
Eliminate exceptions from get_type_arity and get_const_type
Lift mk_abs and mk_comb functions
Lift dest_var and dest_const functions
Lift dest_comb and dest_abs functions
Process type_vars_in_term and variant functions
Eliminate exceptions from vsubst

Process:
1. Find a function throwing exceptions
2. Make it safe by using Choice.failwith (failing branches),
Choice.bind, etc.
3. Replace "func" by "Choice.get <| func" in NHol project
4. Fix errors which mostly are changing <| to << and adding parentheses
5. Create a commit with all changed files