From ceedac330e36a1785a494dc97d0eb982d20e5429 Mon Sep 17 00:00:00 2001
From: Nikhil Swamy <nikswamy@users.noreply.github.com>
Date: Tue, 27 Aug 2024 23:05:11 -0700
Subject: [PATCH] some fixups following revision of FStar.Options

---
 src/ocaml/plugin/Pulse_RuntimeUtils.ml          | 17 +++++++----------
 .../generated/PulseSyntaxExtension_Desugar.ml   |  4 ++--
 .../PulseSyntaxExtension.Desugar.fst            |  4 ++--
 3 files changed, 11 insertions(+), 14 deletions(-)

diff --git a/src/ocaml/plugin/Pulse_RuntimeUtils.ml b/src/ocaml/plugin/Pulse_RuntimeUtils.ml
index a141d43a5..037f6c801 100755
--- a/src/ocaml/plugin/Pulse_RuntimeUtils.ml
+++ b/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
diff --git a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml
index ade0d2683..8ed4d5b8c 100644
--- a/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml
+++ b/src/ocaml/plugin/generated/PulseSyntaxExtension_Desugar.ml
@@ -2860,7 +2860,7 @@ and (desugar_lambda :
                                              let uu___5 =
                                                let uu___6 =
                                                  let uu___7 =
-                                                   FStar_Options.ext_getv
+                                                   FStar_Options_Ext.get
                                                      "pulse:rvalues" in
                                                  uu___7 <> "" in
                                                if uu___6
@@ -3110,7 +3110,7 @@ and (desugar_decl :
                                                         let uu___6 =
                                                           let uu___7 =
                                                             let uu___8 =
-                                                              FStar_Options.ext_getv
+                                                              FStar_Options_Ext.get
                                                                 "pulse:rvalues" in
                                                             uu___8 <> "" in
                                                           if uu___7
diff --git a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst b/src/syntax_extension/PulseSyntaxExtension.Desugar.fst
index f649a8cc9..7bce7cfe1 100644
--- a/src/syntax_extension/PulseSyntaxExtension.Desugar.fst
+++ b/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