diff --git a/src/haz3lcore/dynamics/Elaborator.re b/src/haz3lcore/dynamics/Elaborator.re
index debdfbe975..b72067c38b 100644
--- a/src/haz3lcore/dynamics/Elaborator.re
+++ b/src/haz3lcore/dynamics/Elaborator.re
@@ -148,7 +148,7 @@ let rec dhexp_of_uexp =
     dhexp_of_uexp(m, uexp, in_filter);
   };
   switch (Id.Map.find_opt(Term.UExp.rep_id(uexp), m)) {
-  | Some(InfoExp({mode, self, ctx, ancestors, _})) =>
+  | Some(InfoExp({mode, self, ctx, ancestors, co_ctx, _})) =>
     let err_status = Info.status_exp(ctx, mode, self);
     let id = Term.UExp.rep_id(uexp); /* NOTE: using term uids for hole ids */
     let+ d: DHExp.t =
@@ -252,7 +252,12 @@ let rec dhexp_of_uexp =
         let* ddef = dhexp_of_uexp(m, def);
         let* dbody = dhexp_of_uexp(m, body);
         let+ ty = fixed_pat_typ(m, p);
-        if (!Statics.is_recursive(ctx, p, def, ty)) {
+        let is_recursive =
+          Statics.is_recursive(ctx, p, def, ty)
+          && Term.UPat.get_bindings(p)
+          |> Option.get
+          |> List.exists(f => VarMap.lookup(co_ctx, f) != None);
+        if (!is_recursive) {
           /* not recursive */
           DHExp.Let(
             dp,
diff --git a/src/haz3lcore/dynamics/EvaluatorStep.re b/src/haz3lcore/dynamics/EvaluatorStep.re
index 230c4dcf53..6956ed7eef 100644
--- a/src/haz3lcore/dynamics/EvaluatorStep.re
+++ b/src/haz3lcore/dynamics/EvaluatorStep.re
@@ -150,15 +150,6 @@ module Decompose = {
   module Decomp = Transition(DecomposeEVMode);
   let rec decompose = (state, env, exp) => {
     switch (exp) {
-    | DHExp.Filter(flt, d1) =>
-      DecomposeEVMode.(
-        {
-          let. _ = otherwise(env, (d1) => (Filter(flt, d1): DHExp.t))
-          and. d1 =
-            req_final(decompose(state, env), d1 => Filter(flt, d1), d1);
-          Step({apply: () => d1, kind: CompleteFilter, value: true});
-        }
-      )
     | _ => Decomp.transition(decompose, state, env, exp)
     };
   };
@@ -362,12 +353,219 @@ let decompose = (d: DHExp.t) => {
   Decompose.Result.unbox(rs);
 };
 
-let evaluate_with_history = d => {
+let rec matches =
+        (
+          env: ClosureEnvironment.t,
+          flt: FilterEnvironment.t,
+          ctx: EvalCtx.t,
+          exp: DHExp.t,
+          act: FilterAction.t,
+          idx: int,
+        )
+        : (FilterAction.t, int, EvalCtx.t) => {
+  let composed = compose(ctx, exp);
+  let (pact, pidx) = (act, idx);
+  let (mact, midx) = FilterMatcher.matches(~env, ~exp=composed, ~act, flt);
+  let (act, idx) =
+    switch (ctx) {
+    | Filter(_, _) => (pact, pidx)
+    | _ => midx > pidx ? (mact, midx) : (pact, pidx)
+    };
+  let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => {
+    (a, i, f(c));
+  };
+  let (let+) = map;
+  let (ract, ridx, rctx) =
+    switch (ctx) {
+    | Mark => (act, idx, EvalCtx.Mark)
+    | Closure(env, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Closure(env, ctx);
+    | Filter(Filter(flt'), ctx) =>
+      let flt = flt |> FilterEnvironment.extends(flt');
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Filter(Filter(flt'), ctx);
+    | Filter(Residue(idx', act'), ctx) =>
+      let (ract, ridx, rctx) =
+        if (idx > idx') {
+          matches(env, flt, ctx, exp, act, idx);
+        } else {
+          matches(env, flt, ctx, exp, act', idx');
+        };
+      if (act' |> snd == All) {
+        (ract, ridx, Filter(Residue(idx', act'), rctx));
+      } else {
+        (ract, ridx, rctx);
+      };
+    | Sequence1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Sequence1(ctx, d2);
+    | Sequence2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Sequence2(d1, ctx);
+    | Let1(d1, ctx, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Let1(d1, ctx, d3);
+    | Let2(d1, d2, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Let2(d1, d2, ctx);
+    | Module1(d1, ctx, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Module1(d1, ctx, d3);
+    | Module2(d1, d2, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Module2(d1, d2, ctx);
+    | Dot1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Dot1(ctx, d2);
+    | Dot2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Dot2(d1, ctx);
+    | Fun(dp, ty, ctx, name) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Fun(dp, ty, ctx, name);
+    | FixF(name, ty, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      FixF(name, ty, ctx);
+    | Ap1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Ap1(ctx, d2);
+    | Ap2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Ap2(d1, ctx);
+    | IfThenElse1(c, ctx, d2, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      IfThenElse1(c, ctx, d2, d3);
+    | IfThenElse2(c, d1, ctx, d3) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      IfThenElse2(c, d1, ctx, d3);
+    | IfThenElse3(c, d1, d2, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      IfThenElse3(c, d1, d2, ctx);
+    | BinBoolOp1(op, ctx, d1) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinBoolOp1(op, ctx, d1);
+    | BinBoolOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinBoolOp2(op, d1, ctx);
+    | BinIntOp1(op, ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinIntOp1(op, ctx, d2);
+    | BinIntOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinIntOp2(op, d1, ctx);
+    | BinFloatOp1(op, ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinFloatOp1(op, ctx, d2);
+    | BinFloatOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinFloatOp2(op, d1, ctx);
+    | BinStringOp1(op, ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinStringOp1(op, ctx, d2);
+    | BinStringOp2(op, d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      BinStringOp2(op, d1, ctx);
+    | Tuple(ctx, ds) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Tuple(ctx, ds);
+    | ApBuiltin(name, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ApBuiltin(name, ctx);
+    | Test(id, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Test(id, ctx);
+    | ListLit(u, i, ty, ctx, ds) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ListLit(u, i, ty, ctx, ds);
+    | Cons1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Cons1(ctx, d2);
+    | Cons2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Cons2(d1, ctx);
+    | ListConcat1(ctx, d2) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ListConcat1(ctx, d2);
+    | ListConcat2(d1, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ListConcat2(d1, ctx);
+    | Prj(ctx, n) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Prj(ctx, n);
+    | NonEmptyHole(e, u, i, ctx) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      NonEmptyHole(e, u, i, ctx);
+    | Cast(ctx, ty, ty') =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      Cast(ctx, ty, ty');
+    | FailedCast(ctx, ty, ty') =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      FailedCast(ctx, ty, ty');
+    | InvalidOperation(ctx, error) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      InvalidOperation(ctx, error);
+    | ConsistentCase(Case(ctx, rs, i)) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ConsistentCase(Case(ctx, rs, i));
+    | ConsistentCaseRule(dexp, dpat, ctx, rs, i) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      ConsistentCaseRule(dexp, dpat, ctx, rs, i);
+    | InconsistentBranches(u, i, Case(ctx, rs, ri)) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      InconsistentBranches(u, i, Case(ctx, rs, ri));
+    | InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      InconsistentBranchesRule(dexp, u, i, dpat, ctx, rs, ri);
+    | TypAp(ctx, ty) =>
+      let+ ctx = matches(env, flt, ctx, exp, act, idx);
+      TypAp(ctx, ty);
+    };
+  switch (ctx) {
+  | Filter(_) => (ract, ridx, rctx)
+  | _ when midx > pidx && mact |> snd == All => (
+      ract,
+      ridx,
+      Filter(Residue(midx, mact), rctx),
+    )
+  | _ => (ract, ridx, rctx)
+  };
+};
+
+let should_hide_eval_obj =
+    (~settings, x: EvalObj.t): (FilterAction.action, EvalObj.t) =>
+  if (should_hide_step_kind(~settings, x.knd)) {
+    (Eval, x);
+  } else {
+    let (act, _, ctx) =
+      matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0);
+    switch (act) {
+    | (Eval, _) => (Eval, {...x, ctx})
+    | (Step, _) => (Step, {...x, ctx})
+    };
+  };
+
+let should_hide_step = (~settings, x: step): (FilterAction.action, step) =>
+  if (should_hide_step_kind(~settings, x.knd)) {
+    (Eval, x);
+  } else {
+    let (act, _, ctx) =
+      matches(ClosureEnvironment.empty, [], x.ctx, x.d_loc, (Step, One), 0);
+    switch (act) {
+    | (Eval, _) => (Eval, {...x, ctx})
+    | (Step, _) => (Step, {...x, ctx})
+    };
+  };
+
+let decompose = (~settings, d) =>
+  d |> decompose |> List.map(should_hide_eval_obj(~settings));
+
+let evaluate_with_history = (~settings, d) => {
   let state = ref(EvaluatorState.init);
   let rec go = d =>
-    switch (decompose(d)) {
+    switch (decompose(~settings, d)) {
     | [] => []
-    | [x, ..._] =>
+    | [(_, x), ..._] =>
       switch (take_step(state, x.env, x.d_loc)) {
       | None => []
       | Some(d) =>
diff --git a/src/haz3lcore/dynamics/FilterMatcher.re b/src/haz3lcore/dynamics/FilterMatcher.re
index f3297ad9b6..39153acee1 100644
--- a/src/haz3lcore/dynamics/FilterMatcher.re
+++ b/src/haz3lcore/dynamics/FilterMatcher.re
@@ -1,228 +1,307 @@
 let rec matches_exp =
-        (env: ClosureEnvironment.t, d: DHExp.t, f: DHExp.t): bool => {
-  switch (d, f) {
-  | (Constructor("$e"), _) => failwith("$e in matched expression")
-  | (Constructor("$v"), _) => failwith("$v in matched expression")
-
-  // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps
-  | (FixF(dp, _, dc), f) =>
-    matches_exp(
-      env,
-      Closure(
-        Transition.evaluate_extend_env(Environment.singleton((dp, dc)), env),
-        dc,
-      ),
-      f,
-    )
-  | (d, FixF(fp, _, fc)) =>
-    matches_exp(
-      env,
-      d,
-      Closure(
-        Transition.evaluate_extend_env(Environment.singleton((fp, fc)), env),
-        fc,
-      ),
-    )
-
-  | (_, Constructor("$v")) =>
-    switch (ValueChecker.check_value(env, d)) {
-    | Indet
-    | Value => true
-    | Expr => false
-    }
-
-  | (_, EmptyHole(_))
-  | (_, Constructor("$e")) => true
-
-  | (_, Closure(env, f)) => matches_exp(env, d, f)
-  | (_, Cast(f, _, _)) => matches_exp(env, d, f)
-  | (_, FailedCast(f, _, _)) => matches_exp(env, d, f)
-
-  | (Closure(env, d), _) => matches_exp(env, d, f)
-  | (Cast(d, _, _), _) => matches_exp(env, d, f)
-  | (FailedCast(d, _, _), _) => matches_exp(env, d, f)
-
-  | (BoundVar(dx), BoundVar(fx)) => dx == fx
-  | (BoundVar(dx), _) =>
-    let d =
-      ClosureEnvironment.lookup(env, dx)
-      |> Util.OptUtil.get(() => {
-           print_endline("FreeInvalidVar:" ++ dx);
-           raise(EvaluatorError.Exception(FreeInvalidVar(dx)));
-         });
-    matches_exp(env, d, f);
-  | (_, BoundVar(fx)) =>
-    switch (ClosureEnvironment.lookup(env, fx)) {
-    | Some(f) => matches_exp(env, d, f)
-    | None => false
-    }
-
-  | (EmptyHole(_), _) => false
-
-  | (Filter(df, dd), Filter(ff, fd)) =>
-    DH.DHFilter.fast_equal(df, ff) && matches_exp(env, dd, fd)
-  | (Filter(_), _) => false
-
-  | (BoolLit(dv), BoolLit(fv)) => dv == fv
-  | (BoolLit(_), _) => false
-
-  | (IntLit(dv), IntLit(fv)) => dv == fv
-  | (IntLit(_), _) => false
-
-  | (FloatLit(dv), FloatLit(fv)) => dv == fv
-  | (FloatLit(_), _) => false
-
-  | (StringLit(dv), StringLit(fv)) => dv == fv
-  | (StringLit(_), _) => false
-
-  | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true
-  | (Constructor(dt), Constructor(ft)) => dt == ft
-  | (Constructor(_), _) => false
-
-  | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn
-  | (BuiltinFun(_), _) => false
-
-  | (TypFun(pat1, d1, s1), TypFun(pat2, d2, s2)) =>
-    s1 == s2 && matches_utpat(pat1, pat2) && matches_exp(env, d1, d2)
-  | (TypFun(_), _) => false
-
-  | (Fun(dp1, dty1, d1, dname1), Fun(fp1, fty1, f1, fname1)) =>
-    matches_pat(dp1, fp1)
-    && dty1 == fty1
-    && matches_exp(env, d1, f1)
-    && dname1 == fname1
-  | (Fun(_), _) => false
-
-  | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) =>
-    du == fu && di == fi && dx == fx
-  | (FreeVar(_), _) => false
-
-  | (Let(dp, d1, d2), Let(fp, f1, f2)) =>
-    matches_pat(dp, fp)
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-  | (Let(_), _) => false
-  | (Module(dp, d1, d2), Module(fp, f1, f2)) =>
-    matches_pat(dp, fp)
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-  | (Module(_), _) => false
-  | (Dot(d1, d2), Dot(f1, f2)) =>
-    matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
-  | (Dot(_), _) => false
-  | (ModuleVal(_), ModuleVal(_)) => true
-  | (ModuleVal(_), _) => false
-
-  | (TypAp(d1, t1), TypAp(d2, t2)) =>
-    matches_exp(env, d1, d2) && matches_typ(t1, t2)
-  | (TypAp(_), _) => false
-
-  | (Ap(d1, d2), Ap(f1, f2)) =>
-    matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
-  | (Ap(_), _) => false
-
-  | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) =>
-    dc == fc
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-    && matches_exp(env, d3, f3)
-  | (IfThenElse(_), _) => false
+        (
+          ~denv: ClosureEnvironment.t,
+          d: DHExp.t,
+          ~fenv: ClosureEnvironment.t,
+          f: DHExp.t,
+        )
+        : bool => {
+  let matches_exp = (~denv=denv, ~fenv=fenv, d, f) =>
+    matches_exp(~denv, d, ~fenv, f);
+  if (d == f) {
+    true;
+  } else {
+    switch (d, f) {
+    | (Constructor("$e"), _) => failwith("$e in matched expression")
+    | (Constructor("$v"), _) => failwith("$v in matched expression")
+
+    // HACK[Matt]: ignore fixpoints in comparison, to allow pausing on fixpoint steps
+    | (FixF(dp, dt, dc), FixF(fp, ft, fc)) =>
+      dp == fp
+      && dt == ft
+      && matches_exp(
+           ~denv=denv |> ClosureEnvironment.without_keys([dp]),
+           dc,
+           ~fenv=fenv |> ClosureEnvironment.without_keys([fp]),
+           fc,
+         )
+    | (FixF(dp, _, dc), f) =>
+      matches_exp(~denv=denv |> ClosureEnvironment.without_keys([dp]), dc, f)
+    | (d, FixF(fp, _, fc)) =>
+      matches_exp(d, ~fenv=fenv |> ClosureEnvironment.without_keys([fp]), fc)
+
+    | (_, Constructor("$v")) =>
+      switch (ValueChecker.check_value(denv, d)) {
+      | Indet
+      | Value => true
+      | Expr => false
+      }
 
-  | (Sequence(d1, d2), Sequence(f1, f2)) =>
-    matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
-  | (Sequence(_), _) => false
+    | (_, EmptyHole(_))
+    | (_, Constructor("$e")) => true
 
-  | (Test(id1, d2), Test(id2, f2)) =>
-    id1 == id2 && matches_exp(env, d2, f2)
-  | (Test(_), _) => false
+    | (Cast(d, _, _), Cast(f, _, _)) => matches_exp(d, f)
+    | (Closure(denv, d), Closure(fenv, f)) =>
+      matches_exp(~denv, d, ~fenv, f)
 
-  | (Cons(d1, d2), Cons(f1, f2)) =>
-    matches_exp(env, d1, f1) && matches_exp(env, d2, f2)
-  | (Cons(_), _) => false
+    | (_, Closure(fenv, f)) => matches_exp(~fenv, d, f)
+    | (_, Cast(f, _, _)) => matches_exp(d, f)
+    | (_, FailedCast(f, _, _)) => matches_exp(d, f)
 
-  | (ListLit(_, _, dt, dv), ListLit(_, _, ft, fv)) =>
-    dt == ft
-    && List.fold_left2(
-         (acc, d, f) => acc && matches_exp(env, d, f),
-         true,
-         dv,
-         fv,
-       )
-  | (ListLit(_), _) => false
+    | (Closure(denv, d), _) => matches_exp(~denv, d, f)
+    | (Cast(d, _, _), _) => matches_exp(d, f)
+    | (FailedCast(d, _, _), _) => matches_exp(d, f)
+    | (Filter(Residue(_), d), _) => matches_exp(d, f)
 
-  | (Tuple(dv), Tuple(fv)) =>
-    List.fold_left2(
-      (acc, d, f) => acc && matches_exp(env, d, f),
-      true,
-      dv,
-      fv,
-    )
-  | (Tuple(_), _) => false
-
-  | (BinBoolOp(d_op_bin, d1, d2), BinBoolOp(f_op_bin, f1, f2)) =>
-    d_op_bin == f_op_bin
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-
-  | (BinBoolOp(_), _) => false
-
-  | (BinIntOp(d_op_bin, d1, d2), BinIntOp(f_op_bin, f1, f2)) =>
-    d_op_bin == f_op_bin
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-  | (BinIntOp(_), _) => false
-
-  | (BinFloatOp(d_op_bin, d1, d2), BinFloatOp(f_op_bin, f1, f2)) =>
-    d_op_bin == f_op_bin
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-  | (BinFloatOp(_), _) => false
-
-  | (BinStringOp(d_op_bin, d1, d2), BinStringOp(f_op_bin, f1, f2)) =>
-    d_op_bin == f_op_bin
-    && matches_exp(env, d1, f1)
-    && matches_exp(env, d2, f2)
-  | (BinStringOp(_), _) => false
-
-  | (ListConcat(_), _) => false
-
-  | (
-      ConsistentCase(Case(dscrut, drule, _)),
-      ConsistentCase(Case(fscrut, frule, _)),
-    )
-  | (
-      InconsistentBranches(_, _, Case(dscrut, drule, _)),
-      InconsistentBranches(_, _, Case(fscrut, frule, _)),
-    ) =>
-    matches_exp(env, dscrut, fscrut)
-    && (
+    | (BoundVar(dx), BoundVar(fx))
+        when String.starts_with(dx, ~prefix="__mutual__") =>
+      String.starts_with(fx, ~prefix="__mutual__") && dx == fx
+    | (BoundVar(dx), BoundVar(fx)) =>
       switch (
-        List.fold_left2(
-          (res, drule, frule) => res && matches_rul(env, drule, frule),
-          true,
-          drule,
-          frule,
-        )
+        ClosureEnvironment.lookup(denv, dx),
+        ClosureEnvironment.lookup(fenv, fx),
       ) {
-      | exception (Invalid_argument(_)) => false
-      | res => res
+      | (
+          Some(Fun(_, _, Closure(denv, _), Some(dname)) as d),
+          Some(Fun(_, _, Closure(fenv, _), Some(fname)) as f),
+        )
+          when
+            ClosureEnvironment.lookup(denv, dname) == Some(d)
+            && ClosureEnvironment.lookup(fenv, fname) == Some(f) =>
+        matches_exp(
+          ~denv=ClosureEnvironment.without_keys([dname], denv),
+          d,
+          ~fenv=ClosureEnvironment.without_keys([fname], fenv),
+          f,
+        )
+      | (
+          Some(Fun(_, _, Closure(denv, _), Some(dname)) as d),
+          Some(Fun(_, _, _, Some(fname)) as f),
+        )
+          when
+            ClosureEnvironment.lookup(denv, dname) == Some(d)
+            && ClosureEnvironment.lookup(fenv, fname) == Some(f) =>
+        matches_exp(
+          ~denv=ClosureEnvironment.without_keys([dname], denv),
+          d,
+          ~fenv=ClosureEnvironment.without_keys([fname], fenv),
+          f,
+        )
+      | (
+          Some(Fun(_, _, _, Some(dname)) as d),
+          Some(Fun(_, _, _, Some(fname)) as f),
+        )
+          when
+            ClosureEnvironment.lookup(denv, dname) == Some(d)
+            && ClosureEnvironment.lookup(fenv, fname) == Some(f) =>
+        matches_exp(
+          ~denv=ClosureEnvironment.without_keys([dname], denv),
+          d,
+          ~fenv=ClosureEnvironment.without_keys([fname], fenv),
+          f,
+        )
+      | (
+          Some(Fun(_, _, _, Some(dname)) as d),
+          Some(Fun(_, _, _, Some(fname)) as f),
+        )
+          when
+            ClosureEnvironment.lookup(denv, dname) == Some(d)
+            && ClosureEnvironment.lookup(fenv, fname) == Some(f) =>
+        matches_exp(
+          ~denv=ClosureEnvironment.without_keys([dname], denv),
+          d,
+          ~fenv=ClosureEnvironment.without_keys([fname], denv),
+          f,
+        )
+      | (Some(d), Some(f)) => matches_exp(d, f)
+      | (Some(_), None) => false
+      | (None, Some(_)) => false
+      | (None, None) => true
+      }
+    | (BoundVar(dx), _) =>
+      switch (ClosureEnvironment.lookup(denv, dx)) {
+      | Some(d) => matches_exp(d, f)
+      | None => false
+      }
+    | (_, BoundVar(fx)) =>
+      switch (ClosureEnvironment.lookup(fenv, fx)) {
+      | Some(f) => matches_exp(d, f)
+      | None => false
       }
-    )
-  | (ConsistentCase(_), _)
-  | (InconsistentBranches(_), _) => false
-
-  | (NonEmptyHole(_), _) => false
-  | (InvalidText(_), _) => false
-  | (InvalidOperation(_), _) => false
-
-  | (ApBuiltin(dname, darg), ApBuiltin(fname, farg)) =>
-    dname == fname && matches_exp(env, darg, farg)
-  | (ApBuiltin(_), _) => false
 
-  | (Prj(dv, di), Prj(fv, fi)) => matches_exp(env, dv, fv) && di == fi
-  | (Prj(_), _) => false
+    | (EmptyHole(_), _) => false
+
+    | (Filter(df, dd), Filter(ff, fd)) =>
+      DH.DHFilter.fast_equal(df, ff) && matches_exp(dd, fd)
+    | (Filter(_), _) => false
+
+    | (BoolLit(dv), BoolLit(fv)) => dv == fv
+    | (BoolLit(_), _) => false
+
+    | (IntLit(dv), IntLit(fv)) => dv == fv
+    | (IntLit(_), _) => false
+
+    | (FloatLit(dv), FloatLit(fv)) => dv == fv
+    | (FloatLit(_), _) => false
+
+    | (StringLit(dv), StringLit(fv)) => dv == fv
+    | (StringLit(_), _) => false
+
+    | (Constructor(_), Ap(Constructor("~MVal"), Tuple([]))) => true
+    | (Constructor(dt), Constructor(ft)) => dt == ft
+    | (Constructor(_), _) => false
+
+    | (BuiltinFun(dn), BuiltinFun(fn)) => dn == fn
+    | (BuiltinFun(_), _) => false
+
+    | (TypFun(pat1, d1, s1), TypFun(pat2, d2, s2)) =>
+      s1 == s2 && matches_utpat(pat1, pat2) && matches_exp(d1, d2)
+    | (TypFun(_), _) => false
+
+    | (
+        Fun(dp1, _, Closure(denv, d1), _),
+        Fun(fp1, _, Closure(fenv, f1), _),
+      ) =>
+      matches_fun(~denv, dp1, d1, ~fenv, fp1, f1)
+    | (Fun(dp1, _, Closure(denv, d1), _), Fun(fp1, _, f1, _)) =>
+      matches_fun(~denv, dp1, d1, ~fenv, fp1, f1)
+    | (Fun(dp1, _, d1, _), Fun(fp1, _, Closure(fenv, f1), _)) =>
+      matches_fun(~denv, dp1, d1, ~fenv, fp1, f1)
+    | (Fun(dp1, _, d1, _), Fun(fp1, _, f1, _)) =>
+      matches_fun(~denv, dp1, d1, ~fenv, fp1, f1)
+    | (Fun(_), _) => false
+
+    | (FreeVar(du, di, dx), FreeVar(fu, fi, fx)) =>
+      du == fu && di == fi && dx == fx
+    | (FreeVar(_), _) => false
+
+    | (Let(dp, d1, d2), Let(fp, f1, f2)) =>
+      matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Let(_), _) => false
+    | (Module(dp, d1, d2), Module(fp, f1, f2)) =>
+      matches_pat(dp, fp) && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Module(_), _) => false
+    | (Dot(d1, d2), Dot(f1, f2)) =>
+      matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Dot(_), _) => false
+    | (ModuleVal(a1, b1), ModuleVal(a2, b2)) => a1 == a2 && b1 == b2
+    | (ModuleVal(_), _) => false
+
+    | (TypAp(d1, t1), TypAp(d2, t2)) =>
+      matches_exp(d1, d2) && matches_typ(t1, t2)
+    | (TypAp(_), _) => false
+
+    | (Ap(d1, d2), Ap(f1, f2)) =>
+      matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Ap(_), _) => false
+
+    | (IfThenElse(dc, d1, d2, d3), IfThenElse(fc, f1, f2, f3)) =>
+      dc == fc
+      && matches_exp(d1, f1)
+      && matches_exp(d2, f2)
+      && matches_exp(d3, f3)
+    | (IfThenElse(_), _) => false
+
+    | (Sequence(d1, d2), Sequence(f1, f2)) =>
+      matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Sequence(_), _) => false
+
+    | (Test(id1, d2), Test(id2, f2)) => id1 == id2 && matches_exp(d2, f2)
+    | (Test(_), _) => false
+
+    | (Cons(d1, d2), Cons(f1, f2)) =>
+      matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (Cons(_), _) => false
+
+    | (ListLit(_, _, dt, dv), ListLit(_, _, ft, fv)) =>
+      dt == ft
+      && List.fold_left2(
+           (acc, d, f) => acc && matches_exp(d, f),
+           true,
+           dv,
+           fv,
+         )
+    | (ListLit(_), _) => false
+
+    | (Tuple(dv), Tuple(fv)) =>
+      List.fold_left2((acc, d, f) => acc && matches_exp(d, f), true, dv, fv)
+    | (Tuple(_), _) => false
+
+    | (BinBoolOp(d_op_bin, d1, d2), BinBoolOp(f_op_bin, f1, f2)) =>
+      d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2)
+
+    | (BinBoolOp(_), _) => false
+
+    | (BinIntOp(d_op_bin, d1, d2), BinIntOp(f_op_bin, f1, f2)) =>
+      d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (BinIntOp(_), _) => false
+
+    | (BinFloatOp(d_op_bin, d1, d2), BinFloatOp(f_op_bin, f1, f2)) =>
+      d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (BinFloatOp(_), _) => false
+
+    | (BinStringOp(d_op_bin, d1, d2), BinStringOp(f_op_bin, f1, f2)) =>
+      d_op_bin == f_op_bin && matches_exp(d1, f1) && matches_exp(d2, f2)
+    | (BinStringOp(_), _) => false
+
+    | (ListConcat(_), _) => false
+
+    | (
+        ConsistentCase(Case(dscrut, drule, _)),
+        ConsistentCase(Case(fscrut, frule, _)),
+      )
+    | (
+        InconsistentBranches(_, _, Case(dscrut, drule, _)),
+        InconsistentBranches(_, _, Case(fscrut, frule, _)),
+      ) =>
+      matches_exp(dscrut, fscrut)
+      && (
+        switch (
+          List.fold_left2(
+            (res, drule, frule) =>
+              res && matches_rul(~denv, drule, ~fenv, frule),
+            true,
+            drule,
+            frule,
+          )
+        ) {
+        | exception (Invalid_argument(_)) => false
+        | res => res
+        }
+      )
+    | (ConsistentCase(_), _)
+    | (InconsistentBranches(_), _) => false
+
+    | (NonEmptyHole(_), _) => false
+    | (InvalidText(_), _) => false
+    | (InvalidOperation(_), _) => false
+
+    | (ApBuiltin(dname, darg), ApBuiltin(fname, farg)) =>
+      dname == fname && matches_exp(darg, farg)
+    | (ApBuiltin(_), _) => false
+
+    | (Prj(dv, di), Prj(fv, fi)) => matches_exp(dv, fv) && di == fi
+    | (Prj(_), _) => false
+    };
   };
 }
+and matches_fun =
+    (
+      ~denv: ClosureEnvironment.t,
+      dp: DHPat.t,
+      d: DHExp.t,
+      ~fenv: ClosureEnvironment.t,
+      fp: DHPat.t,
+      f: DHExp.t,
+    ) => {
+  matches_pat(dp, fp)
+  && matches_exp(
+       ~denv=ClosureEnvironment.without_keys(DHPat.bound_vars(dp), denv),
+       d,
+       ~fenv=ClosureEnvironment.without_keys(DHPat.bound_vars(fp), fenv),
+       f,
+     );
+}
 and matches_pat = (d: DHPat.t, f: DHPat.t): bool => {
   switch (d, f) {
   | (_, EmptyHole(_)) => true
@@ -246,7 +325,7 @@ and matches_pat = (d: DHPat.t, f: DHPat.t): bool => {
   | (ListLit(_), _) => false
   | (Constructor(dt), Constructor(ft)) => dt == ft
   | (Constructor(_), _) => false
-  | (Var(dx), Var(fx)) => dx == fx
+  | (Var(_), Var(_)) => true
   | (Var(_), _) => false
   | (Tuple(dl), Tuple(fl)) =>
     switch (
@@ -271,10 +350,10 @@ and matches_pat = (d: DHPat.t, f: DHPat.t): bool => {
 and matches_typ = (d: Typ.t, f: Typ.t) => {
   Typ.eq(d, f);
 }
-and matches_rul = (env, d: DHExp.rule, f: DHExp.rule) => {
+and matches_rul = (~denv, d: DHExp.rule, ~fenv, f: DHExp.rule) => {
   switch (d, f) {
   | (Rule(dp, d), Rule(fp, f)) =>
-    matches_pat(dp, fp) && matches_exp(env, d, f)
+    matches_pat(dp, fp) && matches_exp(~denv, d, ~fenv, f)
   };
 }
 and matches_utpat = (d: Term.UTPat.t, f: Term.UTPat.t): bool => {
@@ -291,7 +370,7 @@ and matches_utpat = (d: Term.UTPat.t, f: Term.UTPat.t): bool => {
 let matches =
     (~env: ClosureEnvironment.t, ~exp: DHExp.t, ~flt: Filter.t)
     : option(FilterAction.t) =>
-  if (matches_exp(env, exp, flt.pat)) {
+  if (matches_exp(~denv=env, exp, ~fenv=env, flt.pat)) {
     Some(flt.act);
   } else {
     None;
diff --git a/src/haz3lcore/dynamics/Stepper.re b/src/haz3lcore/dynamics/Stepper.re
index 1403775a74..9e528af222 100644
--- a/src/haz3lcore/dynamics/Stepper.re
+++ b/src/haz3lcore/dynamics/Stepper.re
@@ -23,7 +23,7 @@ type t = {
   elab: DHExp.t,
   previous: list(step),
   current,
-  next: list(EvalObj.t),
+  next: list((FilterAction.action, EvalObj.t)),
 };
 
 let rec matches =
@@ -42,7 +42,7 @@ let rec matches =
   let (act, idx) =
     switch (ctx) {
     | Filter(_, _) => (pact, pidx)
-    | _ => midx > idx ? (mact, midx) : (pact, pidx)
+    | _ => midx > pidx ? (mact, midx) : (pact, pidx)
     };
   let map = ((a, i, c), f: EvalCtx.t => EvalCtx.t) => {
     (a, i, f(c));
@@ -58,10 +58,15 @@ let rec matches =
       let flt = flt |> FilterEnvironment.extends(flt');
       let+ ctx = matches(env, flt, ctx, exp, act, idx);
       Filter(Filter(flt'), ctx);
-    | Filter(Residue(idx, act), ctx) =>
-      let (ract, ridx, rctx) = matches(env, flt, ctx, exp, act, idx);
-      if (ridx == idx && ract |> snd == All) {
-        (ract, ridx, Filter(Residue(idx, act), rctx));
+    | Filter(Residue(idx', act'), ctx) =>
+      let (ract, ridx, rctx) =
+        if (idx > idx') {
+          matches(env, flt, ctx, exp, act, idx);
+        } else {
+          matches(env, flt, ctx, exp, act', idx');
+        };
+      if (act' |> snd == All) {
+        (ract, ridx, Filter(Residue(idx', act'), rctx));
       } else {
         (ract, ridx, rctx);
       };
@@ -191,7 +196,7 @@ let rec matches =
     };
   switch (ctx) {
   | Filter(_) => (ract, ridx, rctx)
-  | _ when midx == ridx && midx > pidx && mact |> snd == All => (
+  | _ when midx > pidx && mact |> snd == All => (
       ract,
       ridx,
       Filter(Residue(midx, mact), rctx),
@@ -202,7 +207,7 @@ let rec matches =
 
 let should_hide_eval_obj =
     (~settings, x: EvalObj.t): (FilterAction.action, EvalObj.t) =>
-  if (should_hide_step(~settings, x.knd)) {
+  if (should_hide_step_kind(~settings, x.knd)) {
     (Eval, x);
   } else {
     let (act, _, ctx) =
@@ -214,7 +219,7 @@ let should_hide_eval_obj =
   };
 
 let should_hide_step = (~settings, x: step): (FilterAction.action, step) =>
-  if (should_hide_step(~settings, x.knd)) {
+  if (should_hide_step_kind(~settings, x.knd)) {
     (Eval, x);
   } else {
     let (act, _, ctx) =
@@ -239,7 +244,7 @@ let current_expr = (s: t) =>
 
 let step_pending = (idx: int, {elab, previous, current, next}: t) => {
   // TODO[Matt]: change to nth_opt after refactor
-  let eo = List.nth(next, idx);
+  let eo = List.nth(next, idx) |> snd;
   switch (current) {
   | StepperOK(d, s) => {
       elab,
@@ -267,31 +272,15 @@ let step_pending = (idx: int, {elab, previous, current, next}: t) => {
   };
 };
 
-let init = (elab: DHExp.t) => {
+let init = (~settings, elab: DHExp.t) => {
   {
     elab,
     previous: [],
     current: StepPending(elab, EvaluatorState.init, None),
-    next: decompose(elab),
+    next: decompose(~settings, elab),
   };
 };
 
-let update_result =
-    (
-      (
-        d: DHExp.t,
-        state: EvaluatorState.t,
-        next_eval_objs: list(EvalObj.t),
-        skipped_steps: list(step),
-      ),
-      s: t,
-    ) => {
-  previous: skipped_steps @ s.previous,
-  current: StepperOK(d, state),
-  next: next_eval_objs,
-  elab: s.elab,
-};
-
 let rec evaluate_pending = (~settings, s: t) => {
   switch (s.current) {
   | StepperOK(_)
@@ -311,27 +300,26 @@ let rec evaluate_pending = (~settings, s: t) => {
         ...s.previous,
       ],
       current: StepPending(d', state_ref^, None),
-      next: decompose(d'),
+      next: decompose(~settings, d'),
     }
     |> evaluate_pending(~settings);
   | StepPending(d, state, None) =>
-    let next' = s.next |> List.map(should_hide_eval_obj(~settings));
-    switch (List.find_opt(((act, _)) => act == FilterAction.Eval, next')) {
+    switch (List.find_opt(((act, _)) => act == FilterAction.Eval, s.next)) {
     | Some((_, eo)) =>
       {
         elab: s.elab,
         previous: s.previous,
         current: StepPending(d, state, Some(eo)),
-        next: next' |> List.map(snd),
+        next: s.next,
       }
       |> evaluate_pending(~settings)
     | None => {
         elab: s.elab,
         previous: s.previous,
         current: StepperOK(d, state),
-        next: next' |> List.map(snd),
+        next: s.next,
       }
-    };
+    }
   };
 };
 
@@ -394,7 +382,7 @@ let step_backward = (~settings, s: t) =>
   | None => failwith("cannot step backwards")
   | Some((x, xs)) => {
       current: StepperOK(x.d, x.state),
-      next: decompose(x.d),
+      next: decompose(~settings, x.d),
       previous: xs,
       elab: s.elab,
     }
@@ -491,8 +479,7 @@ let to_persistent: t => persistent =
     }
   | {elab, previous, current, _} => {elab, previous, current};
 
-let from_persistent: persistent => t =
-  ({elab, previous, current}) => {
-    let s = {elab, previous, current, next: []};
-    {elab, previous, current, next: decompose(current_expr(s))};
-  };
+let from_persistent = (~settings, {elab, previous, current}) => {
+  let s = {elab, previous, current, next: []};
+  {elab, previous, current, next: decompose(~settings, current_expr(s))};
+};
diff --git a/src/haz3lcore/dynamics/Transition.re b/src/haz3lcore/dynamics/Transition.re
index a68498754c..1a3fdeed1a 100644
--- a/src/haz3lcore/dynamics/Transition.re
+++ b/src/haz3lcore/dynamics/Transition.re
@@ -804,14 +804,22 @@ module Transition = (EV: EV_MODE) => {
       let. _ = otherwise(env, d1 => FailedCast(d1, t1, t2))
       and. _ = req_final(req(state, env), d1 => FailedCast(d1, t1, t2), d1);
       Indet;
-    | Filter(f1, d1) =>
+    | Filter(Filter({pat: Closure(_), _}) as f1, d1)
+    | Filter(Residue(_) as f1, d1) =>
       let. _ = otherwise(env, d1 => Filter(f1, d1))
       and. d1 = req_final(req(state, env), d1 => Filter(f1, d1), d1);
       Step({apply: () => d1, kind: CompleteFilter, value: true});
+    | Filter(Filter({pat, act}) as f1, d1) =>
+      let. _ = otherwise(env, Filter(f1, d1));
+      Step({
+        apply: () => Filter(Filter({pat: Closure(env, pat), act}), d1),
+        kind: CompleteFilter,
+        value: false,
+      });
     };
 };
 
-let should_hide_step = (~settings: CoreSettings.Evaluation.t) =>
+let should_hide_step_kind = (~settings: CoreSettings.Evaluation.t) =>
   fun
   | LetBind
   | ModuleBind
diff --git a/src/haz3lcore/prog/ModelResult.re b/src/haz3lcore/prog/ModelResult.re
index fe1e40d281..5965cd1c52 100644
--- a/src/haz3lcore/prog/ModelResult.re
+++ b/src/haz3lcore/prog/ModelResult.re
@@ -14,14 +14,14 @@ type t =
 let init_eval = elab =>
   Evaluation({elab, evaluation: ResultPending, previous: ResultPending});
 
-let update_elab = elab =>
+let update_elab = (~settings, elab) =>
   fun
   | NoElab =>
     Evaluation({elab, evaluation: ResultPending, previous: ResultPending})
   | Evaluation({evaluation, _}) =>
     Evaluation({elab, evaluation: ResultPending, previous: evaluation})
   | Stepper({elab: elab2, _}) as s when DHExp.fast_equal(elab, elab2) => s
-  | Stepper(_) => Stepper(Stepper.init(elab));
+  | Stepper(_) => Stepper(Stepper.init(~settings, elab));
 
 let update_stepper = f =>
   fun
@@ -55,10 +55,10 @@ let timeout: t => t =
     Evaluation({...e, evaluation: ResultFail(Timeout), previous: evaluation})
   | Stepper(s) => Stepper(Stepper.timeout(s));
 
-let toggle_stepper =
+let toggle_stepper = (~settings) =>
   fun
   | NoElab => NoElab
-  | Evaluation({elab, _}) => Stepper(Stepper.init(elab))
+  | Evaluation({elab, _}) => Stepper(Stepper.init(~settings, elab))
   | Stepper({elab, _}) =>
     Evaluation({elab, evaluation: ResultPending, previous: ResultPending});
 
@@ -91,7 +91,7 @@ let to_persistent: t => persistent =
   | Evaluation(_) => Evaluation
   | Stepper(s) => Stepper(Stepper.to_persistent(s));
 
-let of_persistent: persistent => t =
+let of_persistent = (~settings) =>
   fun
   | Evaluation => NoElab
-  | Stepper(s) => Stepper(Stepper.from_persistent(s));
+  | Stepper(s) => Stepper(Stepper.from_persistent(~settings, s));
diff --git a/src/haz3lcore/prog/ModelResults.re b/src/haz3lcore/prog/ModelResults.re
index a1814f14ba..cceeb3153d 100644
--- a/src/haz3lcore/prog/ModelResults.re
+++ b/src/haz3lcore/prog/ModelResults.re
@@ -22,7 +22,7 @@ type t = M.t(ModelResult.t);
 let init_eval = (ds: list((Key.t, DHExp.t))): t =>
   ds |> List.to_seq |> of_seq |> map(ModelResult.init_eval);
 
-let update_elabs =
+let update_elabs = (~settings) =>
   List.fold_right(((k, elab), acc) =>
     update(
       k,
@@ -30,7 +30,7 @@ let update_elabs =
         Some(
           v
           |> Option.value(~default=ModelResult.NoElab)
-          |> ModelResult.update_elab(elab),
+          |> ModelResult.update_elab(~settings, elab),
         ),
       acc,
     )
diff --git a/src/haz3lcore/statics/Statics.re b/src/haz3lcore/statics/Statics.re
index b04c92c8b6..68b30bfaf5 100644
--- a/src/haz3lcore/statics/Statics.re
+++ b/src/haz3lcore/statics/Statics.re
@@ -296,7 +296,7 @@ and uexp_to_info_map =
     let (e, m) = go(~mode=Ana(Bool), e, m);
     add(~self=Just(Prod([])), ~co_ctx=e.co_ctx, m);
   | Filter(_, cond, body) =>
-    let (cond, m) = go(~mode, cond, m, ~is_in_filter=true);
+    let (cond, m) = go(~mode=Syn, cond, m, ~is_in_filter=true);
     let (body, m) = go(~mode, body, m);
     add(
       ~self=Just(body.ty),
diff --git a/src/haz3lweb/Export.re b/src/haz3lweb/Export.re
index 7bc711cc34..0aa22384e2 100644
--- a/src/haz3lweb/Export.re
+++ b/src/haz3lweb/Export.re
@@ -22,8 +22,10 @@ type all_f22 = {
 let mk_all = (~instructor_mode, ~log) => {
   let settings = Store.Settings.export();
   let explainThisModel = Store.ExplainThisModel.export();
-  let scratch = Store.Scratch.export();
-  let documentation = Store.Documentation.export();
+  let settings_obj = Store.Settings.load();
+  let scratch = Store.Scratch.export(~settings=settings_obj.core.evaluation);
+  let documentation =
+    Store.Documentation.export(~settings=settings_obj.core.evaluation);
   let exercise =
     Store.Exercise.export(
       ~specs=ExerciseSettings.exercises,
@@ -53,7 +55,7 @@ let import_all = (data, ~specs) => {
   let settings = Store.Settings.import(all.settings);
   Store.ExplainThisModel.import(all.explainThisModel);
   let instructor_mode = settings.instructor_mode;
-  Store.Scratch.import(all.scratch);
+  Store.Scratch.import(~settings=settings.core.evaluation, all.scratch);
   Store.Exercise.import(all.exercise, ~specs, ~instructor_mode);
   Log.import(all.log);
 };
diff --git a/src/haz3lweb/Model.re b/src/haz3lweb/Model.re
index 75ac22a0e4..65c5d519c0 100644
--- a/src/haz3lweb/Model.re
+++ b/src/haz3lweb/Model.re
@@ -56,14 +56,14 @@ let blank =
   mk(Editors.Scratch(0, []), ModelResults.empty, CachedStatics.empty);
 
 let load_editors =
-    (~mode: Settings.mode, ~instructor_mode: bool)
+    (~settings, ~mode: Settings.mode, ~instructor_mode: bool)
     : (Editors.t, ModelResults.t) =>
   switch (mode) {
   | Scratch =>
-    let (idx, slides, results) = Store.Scratch.load();
+    let (idx, slides, results) = Store.Scratch.load(~settings);
     (Scratch(idx, slides), results);
   | Documentation =>
-    let (name, slides, results) = Store.Documentation.load();
+    let (name, slides, results) = Store.Documentation.load(~settings);
     (Documentation(name, slides), results);
   | Exercises =>
     let (n, specs, exercise) =
@@ -90,6 +90,7 @@ let load = (init_model: t): t => {
   let explainThisModel = Store.ExplainThisModel.load();
   let (editors, results) =
     load_editors(
+      ~settings=settings.core.evaluation,
       ~mode=settings.mode,
       ~instructor_mode=settings.instructor_mode,
     );
@@ -112,10 +113,11 @@ let reset = (model: t): t => {
   /* Reset model to default, including in localstorage,
      but don't otherwise erase localstorage, allowing
      e.g. api keys to persist */
-  ignore(Store.Settings.init());
+  let settings = Store.Settings.init();
+  ignore(settings);
   ignore(Store.ExplainThisModel.init());
-  ignore(Store.Scratch.init());
-  ignore(Store.Documentation.init());
+  ignore(Store.Scratch.init(~settings=settings.core.evaluation));
+  ignore(Store.Documentation.init(~settings=settings.core.evaluation));
   ignore(Store.Exercise.init(~instructor_mode=true));
   let new_model = load(blank);
   {
diff --git a/src/haz3lweb/Store.re b/src/haz3lweb/Store.re
index 8156dd975d..0c4ac3fe23 100644
--- a/src/haz3lweb/Store.re
+++ b/src/haz3lweb/Store.re
@@ -121,14 +121,14 @@ module Scratch = {
     |> ModelResults.bindings,
   );
 
-  let of_persistent = ((idx, slides, results): persistent) => {
+  let of_persistent = (~settings, (idx, slides, results): persistent) => {
     (
       idx,
       List.map(ScratchSlide.unpersist, slides),
       results
       |> List.to_seq
       |> ModelResults.of_seq
-      |> ModelResults.map(ModelResult.of_persistent),
+      |> ModelResults.map(ModelResult.of_persistent(~settings)),
     );
   };
 
@@ -144,23 +144,23 @@ module Scratch = {
     JsUtil.set_localstore(save_scratch_key, serialize(scratch));
   };
 
-  let init = () => {
-    let scratch = of_persistent(Init.startup.scratch);
+  let init = (~settings) => {
+    let scratch = of_persistent(~settings, Init.startup.scratch);
     save(scratch);
     scratch;
   };
 
-  let load = () =>
+  let load = (~settings) =>
     switch (JsUtil.get_localstore(save_scratch_key)) {
-    | None => init()
+    | None => init(~settings)
     | Some(data) =>
-      try(deserialize(data)) {
-      | _ => init()
+      try(deserialize(~settings, data)) {
+      | _ => init(~settings)
       }
     };
 
-  let export = () => serialize(load());
-  let import = data => save(deserialize(data));
+  let export = (~settings) => serialize(load(~settings));
+  let import = (~settings, data) => save(deserialize(~settings, data));
 };
 
 module Documentation = {
@@ -186,14 +186,14 @@ module Documentation = {
     |> ModelResults.bindings,
   );
 
-  let of_persistent = ((string, slides, results): persistent) => {
+  let of_persistent = (~settings, (string, slides, results): persistent) => {
     (
       string,
       List.map(unpersist, slides),
       results
       |> List.to_seq
       |> ModelResults.of_seq
-      |> ModelResults.map(ModelResult.of_persistent),
+      |> ModelResults.map(ModelResult.of_persistent(~settings)),
     );
   };
 
@@ -209,23 +209,23 @@ module Documentation = {
     JsUtil.set_localstore(save_documentation_key, serialize(slides));
   };
 
-  let init = () => {
-    let documentation = of_persistent(Init.startup.documentation);
+  let init = (~settings) => {
+    let documentation = of_persistent(~settings, Init.startup.documentation);
     save(documentation);
     documentation;
   };
 
-  let load = () =>
+  let load = (~settings) =>
     switch (JsUtil.get_localstore(save_documentation_key)) {
-    | None => init()
+    | None => init(~settings)
     | Some(data) =>
-      try(deserialize(data)) {
-      | _ => init()
+      try(deserialize(~settings, data)) {
+      | _ => init(~settings)
       }
     };
 
-  let export = () => serialize(load());
-  let import = data => save(deserialize(data));
+  let export = (~settings) => serialize(load(~settings));
+  let import = (~settings, data) => save(deserialize(~settings, data));
 };
 
 module Exercise = {
diff --git a/src/haz3lweb/Update.re b/src/haz3lweb/Update.re
index 260aa6a151..e9d4f46068 100644
--- a/src/haz3lweb/Update.re
+++ b/src/haz3lweb/Update.re
@@ -207,7 +207,10 @@ let schedule_evaluation = (~schedule_action, model: Model.t): unit =>
     if (!ModelResults.is_empty(step_rs)) {
       let new_rs =
         step_rs
-        |> ModelResults.update_elabs(elabs)
+        |> ModelResults.update_elabs(
+             ~settings=model.settings.core.evaluation,
+             elabs,
+           )
         |> ModelResults.run_pending(~settings=model.settings.core);
       schedule_action(UpdateResult(new_rs));
     };
@@ -279,11 +282,15 @@ let switch_exercise_editor =
    this between users. The former is a TODO, currently difficult
    due to the more complex architecture of Exercises. */
 let export_persistent_data = () => {
+  let settings = Store.Settings.load();
   let data: PersistentData.t = {
     documentation:
-      Store.Documentation.load() |> Store.Documentation.to_persistent,
-    scratch: Store.Scratch.load() |> Store.Scratch.to_persistent,
-    settings: Store.Settings.load(),
+      Store.Documentation.load(~settings=settings.core.evaluation)
+      |> Store.Documentation.to_persistent,
+    scratch:
+      Store.Scratch.load(~settings=settings.core.evaluation)
+      |> Store.Scratch.to_persistent,
+    settings,
   };
   let contents =
     "let startup : PersistentData.t = " ++ PersistentData.show(data);
@@ -491,7 +498,9 @@ let rec apply =
                Some(
                  v
                  |> Option.value(~default=NoElab: ModelResult.t)
-                 |> ModelResult.toggle_stepper,
+                 |> ModelResult.toggle_stepper(
+                      ~settings=model.settings.core.evaluation,
+                    ),
                )
              ),
       })
diff --git a/src/haz3lweb/view/StepperView.re b/src/haz3lweb/view/StepperView.re
index 83813b4f0b..2a31bf9f0d 100644
--- a/src/haz3lweb/view/StepperView.re
+++ b/src/haz3lweb/view/StepperView.re
@@ -187,7 +187,7 @@ let stepper_view =
             previous
             |> List.nth_opt(_, 0)
             |> Option.map((x: Stepper.step_with_previous) => x.step),
-          ~next_steps=Stepper.get_next_steps(stepper),
+          ~next_steps=Stepper.get_next_steps(stepper) |> List.map(snd),
           ~hidden_steps=hidden,
           ~result_key,
           d,
diff --git a/test/Test_Elaboration.re b/test/Test_Elaboration.re
index 98d1db0fdd..d584492091 100644
--- a/test/Test_Elaboration.re
+++ b/test/Test_Elaboration.re
@@ -258,15 +258,11 @@ let u9: Term.UExp.t = {
 let d9: DHExp.t =
   Let(
     Var("f"),
-    FixF(
-      "f",
-      Arrow(Int, Int),
-      Fun(
-        Var("x"),
-        Int,
-        BinIntOp(Plus, IntLit(1), BoundVar("x")),
-        Some("f+"),
-      ),
+    Fun(
+      Var("x"),
+      Int,
+      BinIntOp(Plus, IntLit(1), BoundVar("x")),
+      Some("f"),
     ),
     IntLit(55),
   );