let rtb_core_check_term g f e =
  debug g (fun _ ->
    Printf.sprintf "(%s) Calling core_check_term on %s" 
          (T.range_to_string (RU.range_of_term e))
          (T.term_to_string e));
  let res = RTB.core_compute_term_type f e in
  res
let rtb_core_check_term g f e =
debug g
  (fun _ ->
      Printf.sprintf "(%s) Calling core_check_term on %s"
        (T.range_to_string (RU.range_of_term e))
        (T.term_to_string e));
let res = RTB.core_compute_term_type f e in
res
Pulse.Checker.Pure.fst.checked
Pulse.Typing.Util.fsti.checked Pulse.Typing.Env.fsti.checked Pulse.Typing.fst.checked Pulse.Syntax.Printer.fsti.checked Pulse.Syntax.fst.checked Pulse.RuntimeUtils.fsti.checked Pulse.Reflection.Util.fst.checked Pulse.PP.fst.checked prims.fst.checked FStar.Tactics.V2.Builtins.fsti.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Pprint.fsti.checked FStar.Squash.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Printf.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Issue.fsti.checked
Pulse.Checker.Pure.fst
Pulse.Typing.Env.env FStar.Reflection.Types.env FStar.Reflection.Types.term FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.option FStar.Stubs.TypeChecker.Core.tot_or_ghost FStar.Reflection.Types.typ FStar.Tactics.Types.typing_token FStar.Tactics.Types.issues FStar.Tactics.V2.Builtins.core_compute_term_type FStar.Tactics.V2.Builtins.ret_t Prims.unit Pulse.Checker.Pure.debug Prims.string FStar.Printf.sprintf FStar.Tactics.V2.Builtins.range_to_string Pulse.RuntimeUtils.range_of_term FStar.Tactics.V2.Builtins.term_to_string
module Pulse.Checker.Pure
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
module T = FStar.Tactics.V2
open FStar.Tactics.V2
open FStar.Reflection.V2 (* shadow named view *)

open Pulse.Reflection
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Reflection.Util
open Pulse.Typing
module P = Pulse.Syntax.Printer
module RTB = FStar.Tactics.V2.Builtins
module RU = Pulse.RuntimeUtils

let debug (g:env) (msg: unit -> T.Tac string) =
  let tac_debugging = T.debugging () in
  if tac_debugging || RU.debug_at_level (fstar_env g) "refl_tc_callbacks"
  then T.print (print_context g ^ "\n" ^ msg())
val rtb_core_check_term : g: Pulse.Typing.Env.env -> f: FStar.Reflection.Types.env -> e: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (r:
          (FStar.Stubs.TypeChecker.Core.tot_or_ghost * FStar.Reflection.Types.typ)
            {FStar.Tactics.Types.typing_token f e r}) *
      FStar.Tactics.Types.issues)
g: Pulse.Typing.Env.env -> f: FStar.Reflection.Types.env -> e: FStar.Reflection.Types.term
  -> FStar.Tactics.Effect.Tac
    (FStar.Pervasives.Native.option (r:
          (FStar.Stubs.TypeChecker.Core.tot_or_ghost * FStar.Reflection.Types.typ)
            {FStar.Tactics.Types.typing_token f e r}) *
      FStar.Tactics.Types.issues)