some fixups following revision of FStar.Options

src/ocaml/plugin/Pulse_RuntimeUtils.ml

@@ -29,15 +29,12 @@ let disable_admit_smt_queries (f: unit -> 'a utac) : 'a utac =
     )
 let with_extv (k:string) (v:string) (f: unit -> 'a utac) : 'a utac =
   fun ps ->
-    let open FStar_Options in
-    with_saved_options (fun _ ->
-      let v0 = get_option "ext" in
-      let v1 = match v0 with
-               | List l0 -> List (String (k^"="^v) :: l0)
-      in
-      set_option "ext" v1;
-      f () ps
-    )
+    let open FStar_Options_Ext in
+    let x = FStar_Options_Ext.save() in
+    FStar_Options_Ext.set k v;
+    let res = f () ps in
+    FStar_Options_Ext.restore x;
+    res
 let env_set_context (g:FStar_Reflection_Types.env) (c:context) = g
 let print_exn (e:exn) = Printexc.to_string e
 let debug_at_level_no_module (s:string) =
@@ -66,7 +63,7 @@ let env_set_range (e:FStar_Reflection_Types.env) (r:FStar_Range.range) =
 
 let is_pulse_option_set (x:string) : bool =
   let key = ("pulse:"^x) in
-  let value = FStar_Options.ext_getv key in
+  let value = FStar_Options_Ext.get key in
   value <> ""
 
 module U = FStar_Syntax_Util

src/syntax_extension/PulseSyntaxExtension.Desugar.fst

@@ -719,7 +719,7 @@ and desugar_lambda (env:env_t) (l:Sugar.lambda)
         return (env, bs, bvs, Some comp)
     in
     let! body = 
-      if FStar.Options.ext_getv "pulse:rvalues" <> ""
+      if FStar.Options.Ext.get "pulse:rvalues" <> ""
       then LR.transform env body
       else return body
     in
@@ -773,7 +773,7 @@ and desugar_decl (env:env_t)
     let bvs = bvs@bvs' in
     let! comp = desugar_computation_type env ascription in
     let! body = 
-      if FStar.Options.ext_getv "pulse:rvalues" <> ""
+      if FStar.Options.Ext.get "pulse:rvalues" <> ""
       then LR.transform env body
       else return body
     in