val universe_of_now : g:env -> e:term ->
  Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Reflection.V2.Tv_Type u))}) & issues)
let universe_of_now g e =
  T.with_policy SMTSync (fun () ->
    T.universe_of g e)
val universe_of_now : g:env -> e:term ->
  Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Reflection.V2.Tv_Type u))}) & issues)
let universe_of_now g e =
T.with_policy SMTSync (fun () -> T.universe_of g e)
Pulse.Typing.Util.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
Pulse.Typing.Util.fst
FStar.Reflection.Types.env FStar.Tactics.NamedView.term FStar.Tactics.V2.Derived.with_policy FStar.Tactics.V2.Builtins.ret_t FStar.Reflection.Types.universe FStar.Tactics.Types.typing_token FStar.Pervasives.Native.Mktuple2 FStar.Stubs.TypeChecker.Core.tot_or_ghost FStar.Reflection.Types.typ FStar.Stubs.TypeChecker.Core.E_Total FStar.Reflection.V2.Builtins.pack_ln FStar.Reflection.V2.Data.Tv_Type FStar.Tactics.Types.SMTSync Prims.unit FStar.Tactics.V2.Builtins.universe_of FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Tactics.NamedView.universe FStar.Tactics.Types.issues
module Pulse.Typing.Util

module L = FStar.List.Tot
module T = FStar.Tactics.V2

(* Call check_equiv under a SMTSync guard policy *)
let check_equiv_now tcenv t0 t1 =
  T.with_policy SMTSync (fun () ->
    T.check_equiv tcenv t0 t1)
val universe_of_now : g:env -> e:term ->
  Tac (option (u:universe{typing_token g e (E_Total, pack_ln (Reflection.V2.Tv_Type u))}) & issues)
g: FStar.Reflection.Types.env -> e: FStar.Tactics.NamedView.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (u7:
          FStar.Tactics.NamedView.universe
            { FStar.Tactics.Types.typing_token g
                e
                (FStar.Stubs.TypeChecker.Core.E_Total,
                  FStar.Reflection.V2.Builtins.pack_ln (FStar.Reflection.V2.Data.Tv_Type u7)) }) *
      FStar.Tactics.Types.issues)