anchor.diff:    let typecheck tcenv decls =
       let ses, _, _ = FStar.TypeChecker.Tc.tc_decls tcenv decls in
       ses in
  -
  -  let rules =
  -    (match rules with
  -     | Some rules -> rules
  -     | None -> [FStar.TypeChecker.Normalize.Beta;
  -               FStar.TypeChecker.Normalize.Iota;
  -               FStar.TypeChecker.Normalize.Zeta;
  -               FStar.TypeChecker.Normalize.UnfoldUntil SS.Delta_constant])
  -    @ [FStar.TypeChecker.Normalize.Inlining;
  -       FStar.TypeChecker.Normalize.Eager_unfolding;
  -       FStar.TypeChecker.Normalize.Primops] in
   
     run_and_rewind st (fun st ->
       let tcenv = st.repl_env in
  
positive.code:   | CKModuleOrNamespace (modules, namespaces) ->
      run_module_autocomplete st search_term modules namespaces
  
  let run_compute st term rules =
    let run_and_rewind st task =
      let env' = push st.repl_env "#compute" in
      let results = task st in
      pop env' "#compute";
      (results, Inl st) in
  
    let dummy_let_fragment term =
      let dummy_decl = Util.format1 "let __compute_dummy__ = (%s)" term in
      { frag_text = dummy_decl; frag_line = 0; frag_col = 0 } in
  
    let normalize_term tcenv rules t =
      FStar.TypeChecker.Normalize.normalize rules tcenv t in
  
    let find_let_body ses =
      match ses with
  
negative.code:           | Some (univs, def) ->
              let univs, def = Syntax.Subst.open_univ_vars univs def in
              let tcenv = TcEnv.push_univ_vars tcenv univs in
              continuation tcenv def in
          if Options.trace_error () then
            aux ()
          else
            try aux ()
            with | e -> (QueryNOK, (match FStar.Errors.issue_of_exn e with
                                   | Some issue -> JsonStr (FStar.Errors.format_issue issue)
                                   | None -> raise e)))
  
  let run_compute st term rules =
    let rules =
      (match rules with
       | Some rules -> rules
       | None -> [FStar.TypeChecker.Normalize.Beta;
                 FStar.TypeChecker.Normalize.Iota;
                 FStar.TypeChecker.Normalize.Zeta;
                 FStar.TypeChecker.Normalize.UnfoldUntil SS.Delta_constant])
      @ [FStar.TypeChecker.Normalize.Inlining;
         FStar.TypeChecker.Normalize.Eager_unfolding;
         FStar.TypeChecker.Normalize.Primops] in
  
    let normalize_term tcenv rules t =
      FStar.TypeChecker.Normalize.normalize rules tcenv t in
  
    run_with_parsed_and_tc_term st term 0 0 (fun tcenv def ->
        let normalized = normalize_term tcenv rules def in
        (QueryOK, JsonStr (term_to_string tcenv normalized)))
  
  type search_term' =
  | NameContainsStr of string
  