Steel.Effect.common: use static quote to be able to run natively

FStarLang · Sep 30, 2020 · 4592e12 · 4592e12
1 parent 43beaca
commit 4592e12
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/ulib/experimental/Steel.Effect.Common.fst b/ulib/experimental/Steel.Effect.Common.fst
@@ -906,7 +906,7 @@ let rec solve_subcomp_pre (l:list goal) : Tac unit =
     match f with
     | App _ t ->
         let hd, args = collect_app t in
-        if term_eq hd (quote delay) then (focus (fun _ ->
+        if term_eq hd (`delay) then (focus (fun _ ->
           norm [delta_only [`%delay]];
           or_else (fun _ -> apply_lemma (`emp_unit_variant))
                   (fun _ ->
@@ -941,7 +941,7 @@ let rec solve_subcomp_post (l:list goal) : Tac unit =
     match f with
     | App _ t ->
         let hd, args = collect_app t in
-        if term_eq hd (quote annot_sub_post) then (focus (fun _ ->
+        if term_eq hd (`annot_sub_post) then (focus (fun _ ->
           or_else (fun _ -> apply_lemma (`emp_unit_variant_forall))
                   (fun _ ->
                      norm [delta_only [`%annot_sub_post]];
@@ -1025,9 +1025,9 @@ let solve_or_delay (g:goal) : Tac bool =
   match f with
   | App _ t ->
       let hd, args = collect_app t in
-      if term_eq hd (quote annot_sub_post) then false
-      else if term_eq hd (quote can_be_split) then solve_can_be_split args
-      else if term_eq hd (quote can_be_split_forall) then solve_can_be_split_forall args
+      if term_eq hd (`annot_sub_post) then false
+      else if term_eq hd (`can_be_split) then solve_can_be_split args
+      else if term_eq hd (`can_be_split_forall) then solve_can_be_split_forall args
       else false
   | Comp (Eq _) l r ->
     let lnbr = List.Tot.length (FStar.Reflection.Builtins.free_uvars l) in