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 dsenv, tcenv = st.repl_env in
  
positive.code:   | "full" -> FullCheck
    | _ -> js_fail "push_kind" s
  
  type query' =
  | Exit
  | DescribeProtocol
  
negative.code:                                        assoc "[location]" "line" loc |> js_int,
                                         assoc "[location]" "column" loc |> js_int)),
                                  arg "requested-info" |> js_list js_str)
             | "compute" -> Compute (arg "term" |> js_str,
                                    try_arg "rules"
                                      |> Util.map_option (js_list js_reductionrule))
             | "search" -> Search (arg "terms" |> js_str)
             | _ -> ProtocolViolation (Util.format1 "Unknown query '%s'" query) }
    with
  