tactics: exposing ext_options/all_ext_options

[mtzguido]

cc @nikswamy, there's no way to access them from tactics otherwise as of yet, right?

Also I wonder if it would be more future proof to provide a KV interface, such as:

val get_ext : key:string -> string

And writing --ext k=v to define one. The key could use dots to separate namespaces purely as a convention. We could maybe define an ext_options analogue that looks at the prefix of each key to decide which pairs to return.

[mtzguido]

Updated this PR to implement the KV semantics.