diff --git a/ocaml/fstar-lib/generated/FStar_Ident.ml b/ocaml/fstar-lib/generated/FStar_Ident.ml
index 12a4a586999..0f4ac423ece 100644
--- a/ocaml/fstar-lib/generated/FStar_Ident.ml
+++ b/ocaml/fstar-lib/generated/FStar_Ident.ml
@@ -149,4 +149,8 @@ let (hasrange_lident : lident FStar_Class_HasRange.hasRange) =
              FStar_Class_HasRange.setPos hasrange_ident rng id.ident in
            { ns = (id.ns); ident = uu___; nsstr = (id.nsstr); str = (id.str)
            })
-  }
\ No newline at end of file
+  }
+let (deq_ident : ident FStar_Class_Deq.deq) =
+  { FStar_Class_Deq.op_Equals_Question = ident_equals }
+let (deq_lident : lident FStar_Class_Deq.deq) =
+  { FStar_Class_Deq.op_Equals_Question = lid_equals }
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
index b2b3d8281f1..0c1cde49d5e 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_Dep.ml
@@ -136,7 +136,7 @@ let (module_name_of_file : Prims.string -> Prims.string) =
     | FStar_Pervasives_Native.None ->
         let uu___1 =
           let uu___2 =
-            FStar_Compiler_Util.format1 "not a valid FStar file: %s" f in
+            FStar_Compiler_Util.format1 "Not a valid FStar file: '%s'" f in
           (FStar_Errors_Codes.Fatal_NotValidFStarFile, uu___2) in
         FStar_Errors.raise_err uu___1
 let (lowercase_module_name : Prims.string -> Prims.string) =
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
index 08a1555e506..a0948f535e3 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Syntax.ml
@@ -2321,6 +2321,8 @@ let (deq_univ_name : univ_name FStar_Class_Deq.deq) =
        fun y ->
          let uu___ = order_univ_name x y in
          FStar_Compiler_Order.order_from_int uu___)
+let (deq_delta_depth : delta_depth FStar_Class_Deq.deq) =
+  { FStar_Class_Deq.op_Equals_Question = (fun x -> fun y -> x = y) }
 let (ord_bv : bv FStar_Class_Ord.ord) =
   ord_instance_from_cmp
     (fun x ->
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
index 758214f6332..25c2396645a 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
@@ -551,6 +551,170 @@ let (steps_to_string : fsteps -> Prims.string) =
     FStar_Compiler_Util.format
       "{\nbeta = %s;\niota = %s;\nzeta = %s;\nzeta_full = %s;\nweak = %s;\nhnf  = %s;\nprimops = %s;\ndo_not_unfold_pure_lets = %s;\nunfold_until = %s;\nunfold_only = %s;\nunfold_fully = %s;\nunfold_attr = %s;\nunfold_qual = %s;\nunfold_namespace = %s;\nunfold_tac = %s;\npure_subterms_within_computations = %s;\nsimplify = %s;\nerase_universes = %s;\nallow_unbound_universes = %s;\nreify_ = %s;\ncompress_uvars = %s;\nno_full_norm = %s;\ncheck_no_uvars = %s;\nunmeta = %s;\nunascribe = %s;\nin_full_norm_request = %s;\nweakly_reduce_scrutinee = %s;\nfor_extraction = %s;\nunrefine = %s;\ndefault_univs_to_zero = %s;\n}"
       uu___
+let (deq_fsteps : fsteps FStar_Class_Deq.deq) =
+  {
+    FStar_Class_Deq.op_Equals_Question =
+      (fun f1 ->
+         fun f2 ->
+           ((((((((((((((((((((((((((((((FStar_Class_Deq.op_Equals_Question
+                                           (FStar_Class_Ord.ord_eq
+                                              FStar_Class_Ord.ord_bool)
+                                           f1.beta f2.beta)
+                                          &&
+                                          (FStar_Class_Deq.op_Equals_Question
+                                             (FStar_Class_Ord.ord_eq
+                                                FStar_Class_Ord.ord_bool)
+                                             f1.iota f2.iota))
+                                         &&
+                                         (FStar_Class_Deq.op_Equals_Question
+                                            (FStar_Class_Ord.ord_eq
+                                               FStar_Class_Ord.ord_bool)
+                                            f1.zeta f2.zeta))
+                                        &&
+                                        (FStar_Class_Deq.op_Equals_Question
+                                           (FStar_Class_Ord.ord_eq
+                                              FStar_Class_Ord.ord_bool)
+                                           f1.zeta_full f2.zeta_full))
+                                       &&
+                                       (FStar_Class_Deq.op_Equals_Question
+                                          (FStar_Class_Ord.ord_eq
+                                             FStar_Class_Ord.ord_bool)
+                                          f1.weak f2.weak))
+                                      &&
+                                      (FStar_Class_Deq.op_Equals_Question
+                                         (FStar_Class_Ord.ord_eq
+                                            FStar_Class_Ord.ord_bool) 
+                                         f1.hnf f2.hnf))
+                                     &&
+                                     (FStar_Class_Deq.op_Equals_Question
+                                        (FStar_Class_Ord.ord_eq
+                                           FStar_Class_Ord.ord_bool)
+                                        f1.primops f2.primops))
+                                    &&
+                                    (FStar_Class_Deq.op_Equals_Question
+                                       (FStar_Class_Ord.ord_eq
+                                          FStar_Class_Ord.ord_bool)
+                                       f1.do_not_unfold_pure_lets
+                                       f2.do_not_unfold_pure_lets))
+                                   &&
+                                   (FStar_Class_Deq.op_Equals_Question
+                                      (FStar_Class_Deq.deq_option
+                                         FStar_Syntax_Syntax.deq_delta_depth)
+                                      f1.unfold_until f2.unfold_until))
+                                  &&
+                                  (FStar_Class_Deq.op_Equals_Question
+                                     (FStar_Class_Ord.ord_eq
+                                        (FStar_Class_Ord.ord_option
+                                           (FStar_Class_Ord.ord_list
+                                              FStar_Syntax_Syntax.ord_fv)))
+                                     f1.unfold_only f2.unfold_only))
+                                 &&
+                                 (FStar_Class_Deq.op_Equals_Question
+                                    (FStar_Class_Ord.ord_eq
+                                       (FStar_Class_Ord.ord_option
+                                          (FStar_Class_Ord.ord_list
+                                             FStar_Syntax_Syntax.ord_fv)))
+                                    f1.unfold_fully f2.unfold_fully))
+                                &&
+                                (FStar_Class_Deq.op_Equals_Question
+                                   (FStar_Class_Ord.ord_eq
+                                      (FStar_Class_Ord.ord_option
+                                         (FStar_Class_Ord.ord_list
+                                            FStar_Syntax_Syntax.ord_fv)))
+                                   f1.unfold_attr f2.unfold_attr))
+                               &&
+                               (FStar_Class_Deq.op_Equals_Question
+                                  (FStar_Class_Ord.ord_eq
+                                     (FStar_Class_Ord.ord_option
+                                        (FStar_Class_Ord.ord_list
+                                           FStar_Class_Ord.ord_string)))
+                                  f1.unfold_qual f2.unfold_qual))
+                              &&
+                              (FStar_Class_Deq.op_Equals_Question
+                                 (FStar_Class_Ord.ord_eq
+                                    (FStar_Class_Ord.ord_option
+                                       (FStar_Class_Ord.ord_tuple2
+                                          (FStar_Class_Ord.ord_list
+                                             (FStar_Class_Ord.ord_tuple2
+                                                (FStar_Class_Ord.ord_list
+                                                   FStar_Class_Ord.ord_string)
+                                                FStar_Class_Ord.ord_bool))
+                                          FStar_Class_Ord.ord_bool)))
+                                 f1.unfold_namespace f2.unfold_namespace))
+                             &&
+                             (FStar_Class_Deq.op_Equals_Question
+                                (FStar_Class_Ord.ord_eq
+                                   FStar_Class_Ord.ord_bool) f1.unfold_tac
+                                f2.unfold_tac))
+                            &&
+                            (FStar_Class_Deq.op_Equals_Question
+                               (FStar_Class_Ord.ord_eq
+                                  FStar_Class_Ord.ord_bool)
+                               f1.pure_subterms_within_computations
+                               f2.pure_subterms_within_computations))
+                           &&
+                           (FStar_Class_Deq.op_Equals_Question
+                              (FStar_Class_Ord.ord_eq
+                                 FStar_Class_Ord.ord_bool) f1.simplify
+                              f2.simplify))
+                          &&
+                          (FStar_Class_Deq.op_Equals_Question
+                             (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                             f1.erase_universes f2.erase_universes))
+                         &&
+                         (FStar_Class_Deq.op_Equals_Question
+                            (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                            f1.allow_unbound_universes
+                            f2.allow_unbound_universes))
+                        &&
+                        (FStar_Class_Deq.op_Equals_Question
+                           (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                           f1.reify_ f2.reify_))
+                       &&
+                       (FStar_Class_Deq.op_Equals_Question
+                          (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                          f1.compress_uvars f2.compress_uvars))
+                      &&
+                      (FStar_Class_Deq.op_Equals_Question
+                         (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                         f1.no_full_norm f2.no_full_norm))
+                     &&
+                     (FStar_Class_Deq.op_Equals_Question
+                        (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                        f1.check_no_uvars f2.check_no_uvars))
+                    &&
+                    (FStar_Class_Deq.op_Equals_Question
+                       (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                       f1.unmeta f2.unmeta))
+                   &&
+                   (FStar_Class_Deq.op_Equals_Question
+                      (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                      f1.unascribe f2.unascribe))
+                  &&
+                  (FStar_Class_Deq.op_Equals_Question
+                     (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                     f1.in_full_norm_request f2.in_full_norm_request))
+                 &&
+                 (FStar_Class_Deq.op_Equals_Question
+                    (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                    f1.weakly_reduce_scrutinee f2.weakly_reduce_scrutinee))
+                &&
+                (FStar_Class_Deq.op_Equals_Question
+                   (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                   f1.nbe_step f2.nbe_step))
+               &&
+               (FStar_Class_Deq.op_Equals_Question
+                  (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                  f1.for_extraction f2.for_extraction))
+              &&
+              (FStar_Class_Deq.op_Equals_Question
+                 (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                 f1.unrefine f2.unrefine))
+             &&
+             (FStar_Class_Deq.op_Equals_Question
+                (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+                f1.default_univs_to_zero f2.default_univs_to_zero))
+  }
 let (default_steps : fsteps) =
   {
     beta = true;
@@ -2334,7 +2498,9 @@ let (translate_norm_steps :
     let s1 = FStar_Compiler_List.concatMap translate_norm_step s in
     let add_exclude s2 z =
       let uu___ =
-        FStar_Compiler_Util.for_some (FStar_TypeChecker_Env.eq_step z) s2 in
+        FStar_Compiler_Util.for_some
+          (FStar_Class_Deq.op_Equals_Question FStar_TypeChecker_Env.deq_step
+             z) s2 in
       if uu___ then s2 else (FStar_TypeChecker_Env.Exclude z) :: s2 in
     let s2 = FStar_TypeChecker_Env.Beta :: s1 in
     let s3 = add_exclude s2 FStar_TypeChecker_Env.Zeta in
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
index d4df26a0200..16fbc495b42 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
@@ -162,23 +162,33 @@ let rec (eq_step : step -> step -> Prims.bool) =
       | (Exclude s11, Exclude s21) -> eq_step s11 s21
       | (UnfoldUntil s11, UnfoldUntil s21) -> s11 = s21
       | (UnfoldOnly lids1, UnfoldOnly lids2) ->
-          ((FStar_Compiler_List.length lids1) =
-             (FStar_Compiler_List.length lids2))
-            &&
-            (FStar_Compiler_List.forall2 FStar_Ident.lid_equals lids1 lids2)
+          FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Ord.ord_eq
+               (FStar_Class_Ord.ord_list FStar_Syntax_Syntax.ord_fv)) lids1
+            lids2
       | (UnfoldFully lids1, UnfoldFully lids2) ->
-          ((FStar_Compiler_List.length lids1) =
-             (FStar_Compiler_List.length lids2))
-            &&
-            (FStar_Compiler_List.forall2 FStar_Ident.lid_equals lids1 lids2)
+          FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Ord.ord_eq
+               (FStar_Class_Ord.ord_list FStar_Syntax_Syntax.ord_fv)) lids1
+            lids2
       | (UnfoldAttr lids1, UnfoldAttr lids2) ->
-          ((FStar_Compiler_List.length lids1) =
-             (FStar_Compiler_List.length lids2))
-            &&
-            (FStar_Compiler_List.forall2 FStar_Ident.lid_equals lids1 lids2)
-      | (UnfoldQual strs1, UnfoldQual strs2) -> strs1 = strs2
-      | (UnfoldNamespace strs1, UnfoldNamespace strs2) -> strs1 = strs2
+          FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Ord.ord_eq
+               (FStar_Class_Ord.ord_list FStar_Syntax_Syntax.ord_fv)) lids1
+            lids2
+      | (UnfoldQual strs1, UnfoldQual strs2) ->
+          FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Ord.ord_eq
+               (FStar_Class_Ord.ord_list FStar_Class_Ord.ord_string)) strs1
+            strs2
+      | (UnfoldNamespace strs1, UnfoldNamespace strs2) ->
+          FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Ord.ord_eq
+               (FStar_Class_Ord.ord_list FStar_Class_Ord.ord_string)) strs1
+            strs2
       | uu___ -> false
+let (deq_step : step FStar_Class_Deq.deq) =
+  { FStar_Class_Deq.op_Equals_Question = eq_step }
 type sig_binding =
   (FStar_Ident.lident Prims.list * FStar_Syntax_Syntax.sigelt)
 type delta_level =
@@ -199,6 +209,20 @@ let (uu___is_Unfold : delta_level -> Prims.bool) =
 let (__proj__Unfold__item___0 :
   delta_level -> FStar_Syntax_Syntax.delta_depth) =
   fun projectee -> match projectee with | Unfold _0 -> _0
+let (deq_delta_level : delta_level FStar_Class_Deq.deq) =
+  {
+    FStar_Class_Deq.op_Equals_Question =
+      (fun x ->
+         fun y ->
+           match (x, y) with
+           | (NoDelta, NoDelta) -> true
+           | (InliningDelta, InliningDelta) -> true
+           | (Eager_unfolding_only, Eager_unfolding_only) -> true
+           | (Unfold x1, Unfold y1) ->
+               FStar_Class_Deq.op_Equals_Question
+                 FStar_Syntax_Syntax.deq_delta_depth x1 y1
+           | uu___ -> false)
+  }
 type name_prefix = FStar_Ident.path
 type proof_namespace = (name_prefix * Prims.bool) Prims.list
 type cached_elt =
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
index e16ebf878fb..7ad5deddd13 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Normalize.ml
@@ -191,6 +191,22 @@ let (head_of : FStar_Syntax_Syntax.term -> FStar_Syntax_Syntax.term) =
   fun t ->
     let uu___ = FStar_Syntax_Util.head_and_args_full t in
     match uu___ with | (hd, uu___1) -> hd
+let (cfg_equivalent :
+  FStar_TypeChecker_Cfg.cfg -> FStar_TypeChecker_Cfg.cfg -> Prims.bool) =
+  fun c1 ->
+    fun c2 ->
+      ((FStar_Class_Deq.op_Equals_Question FStar_TypeChecker_Cfg.deq_fsteps
+          c1.FStar_TypeChecker_Cfg.steps c2.FStar_TypeChecker_Cfg.steps)
+         &&
+         (FStar_Class_Deq.op_Equals_Question
+            (FStar_Class_Deq.deq_list FStar_TypeChecker_Env.deq_delta_level)
+            c1.FStar_TypeChecker_Cfg.delta_level
+            c2.FStar_TypeChecker_Cfg.delta_level))
+        &&
+        (FStar_Class_Deq.op_Equals_Question
+           (FStar_Class_Ord.ord_eq FStar_Class_Ord.ord_bool)
+           c1.FStar_TypeChecker_Cfg.normalize_pure_lets
+           c2.FStar_TypeChecker_Cfg.normalize_pure_lets)
 let read_memo :
   'a .
     FStar_TypeChecker_Cfg.cfg ->
@@ -202,8 +218,9 @@ let read_memo :
       let uu___ = FStar_Compiler_Effect.op_Bang r in
       match uu___ with
       | FStar_Pervasives_Native.Some (cfg', a1) when
-          cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg ||
-            (FStar_Compiler_Util.physical_equality cfg cfg')
+          (cfg.FStar_TypeChecker_Cfg.compat_memo_ignore_cfg ||
+             (FStar_Compiler_Util.physical_equality cfg cfg'))
+            || (cfg_equivalent cfg' cfg)
           -> FStar_Pervasives_Native.Some a1
       | uu___1 -> FStar_Pervasives_Native.None
 let set_memo :
@@ -1758,7 +1775,8 @@ let (rejig_norm_request :
 let (is_nbe_request : FStar_TypeChecker_Env.step Prims.list -> Prims.bool) =
   fun s ->
     FStar_Compiler_Util.for_some
-      (FStar_TypeChecker_Env.eq_step FStar_TypeChecker_Env.NBE) s
+      (FStar_Class_Deq.op_Equals_Question FStar_TypeChecker_Env.deq_step
+         FStar_TypeChecker_Env.NBE) s
 let get_norm_request :
   'uuuuu .
     FStar_TypeChecker_Cfg.cfg ->
@@ -10322,7 +10340,7 @@ let (get_n_binders :
       FStar_Syntax_Syntax.term ->
         (FStar_Syntax_Syntax.binder Prims.list * FStar_Syntax_Syntax.comp))
   = fun env1 -> fun n -> fun t -> get_n_binders' env1 [] n t
-let (uu___3995 : unit) =
+let (uu___3997 : unit) =
   FStar_Compiler_Effect.op_Colon_Equals __get_n_binders get_n_binders'
 let (maybe_unfold_head_fv :
   FStar_TypeChecker_Env.env ->
diff --git a/src/basic/FStar.Ident.fst b/src/basic/FStar.Ident.fst
index 2a61e74eb49..a6d20ae431a 100644
--- a/src/basic/FStar.Ident.fst
+++ b/src/basic/FStar.Ident.fst
@@ -88,3 +88,9 @@ instance hasrange_lident = {
   pos = (fun lid -> Class.HasRange.pos lid.ident);
   setPos = (fun rng id -> { id with ident = setPos rng id.ident });
 }
+instance deq_ident = {
+  (=?) = ident_equals;
+}
+instance deq_lident = {
+  (=?) = lid_equals;
+}
diff --git a/src/basic/FStar.Ident.fsti b/src/basic/FStar.Ident.fsti
index e92c9cbd0f3..f05186d3f71 100644
--- a/src/basic/FStar.Ident.fsti
+++ b/src/basic/FStar.Ident.fsti
@@ -18,6 +18,7 @@ module FStar.Ident
 open FStar.Compiler.Range
 open FStar.Class.Show
 open FStar.Class.HasRange
+open FStar.Class.Deq
 
 (** A (short) identifier for a local name.
  *  e.g. x in `fun x -> ...` *)
@@ -138,3 +139,5 @@ instance val showable_ident  : showable ident
 instance val showable_lident : showable lident
 instance val hasrange_ident  : hasRange ident
 instance val hasrange_lident : hasRange lident
+instance val deq_ident  : deq ident
+instance val deq_lident : deq lident
diff --git a/src/data/FStar.Compiler.Path.fst b/src/data/FStar.Compiler.Path.fst
index b920eec3e28..365fefd0365 100644
--- a/src/data/FStar.Compiler.Path.fst
+++ b/src/data/FStar.Compiler.Path.fst
@@ -32,4 +32,4 @@ let search_forest #a #q {| deq a |} p f =
     | [] -> def
     | (r, q)::rs -> if p `is_under` r then q else aux rs
   in
-  aux roots
\ No newline at end of file
+  aux roots
diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst
index 64df0d88f12..778ce9e01a6 100644
--- a/src/parser/FStar.Parser.Dep.fst
+++ b/src/parser/FStar.Parser.Dep.fst
@@ -125,7 +125,7 @@ let module_name_of_file f =
     | Some longname ->
       longname
     | None ->
-      raise_err (Errors.Fatal_NotValidFStarFile, (Util.format1 "not a valid FStar file: %s" f))
+      raise_err (Errors.Fatal_NotValidFStarFile, (Util.format1 "Not a valid FStar file: '%s'" f))
 
 (* In public interface *)
 let lowercase_module_name f = String.lowercase (module_name_of_file f)
diff --git a/src/syntax/FStar.Syntax.Syntax.fst b/src/syntax/FStar.Syntax.Syntax.fst
index 655de69b68d..15ce4d669b0 100644
--- a/src/syntax/FStar.Syntax.Syntax.fst
+++ b/src/syntax/FStar.Syntax.Syntax.fst
@@ -146,6 +146,10 @@ instance deq_fv : deq lident =
   deq_instance_from_cmp (fun x y -> Order.order_from_int (order_fv x y))
 instance deq_univ_name : deq univ_name =
   deq_instance_from_cmp (fun x y -> Order.order_from_int (order_univ_name x y))
+instance deq_delta_depth : deq delta_depth = {
+  (=?) = (fun x y -> x = y);
+}
+
 instance ord_bv : ord bv =
   ord_instance_from_cmp (fun x y -> Order.order_from_int (order_bv x y))
 instance ord_ident : ord ident =
@@ -510,4 +514,4 @@ instance deq_lazy_kind : deq lazy_kind = {
           | Lazy_embedding _, _
           | _, Lazy_embedding _ -> false
           | _ -> false);
-}
\ No newline at end of file
+}
diff --git a/src/syntax/FStar.Syntax.Syntax.fsti b/src/syntax/FStar.Syntax.Syntax.fsti
index a4aed1f2b17..836253d5ab4 100644
--- a/src/syntax/FStar.Syntax.Syntax.fsti
+++ b/src/syntax/FStar.Syntax.Syntax.fsti
@@ -907,11 +907,12 @@ instance val showable_should_check_uvar : showable should_check_uvar
 
 instance val showable_lazy_kind : showable lazy_kind
 
-instance val deq_lazy_kind : deq lazy_kind
-instance val deq_bv         : deq bv
-instance val deq_ident      : deq ident
-instance val deq_fv         : deq lident
-instance val deq_univ_name  : deq univ_name
+instance val deq_lazy_kind   : deq lazy_kind
+instance val deq_bv          : deq bv
+instance val deq_ident       : deq ident
+instance val deq_fv          : deq lident
+instance val deq_univ_name   : deq univ_name
+instance val deq_delta_depth : deq delta_depth
 
 instance val ord_bv         : ord bv
 instance val ord_ident      : ord ident
diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst
index f647b1a5743..9ad7139968c 100644
--- a/src/typechecker/FStar.TypeChecker.Cfg.fst
+++ b/src/typechecker/FStar.TypeChecker.Cfg.fst
@@ -99,6 +99,41 @@ let steps_to_string f =
     f.default_univs_to_zero |> b;
    ]
 
+instance deq_fsteps : deq fsteps = {
+  (=?) = (fun f1 f2 ->
+            f1.beta =? f2.beta &&
+            f1.iota =? f2.iota &&
+            f1.zeta =? f2.zeta &&
+            f1.zeta_full =? f2.zeta_full &&
+            f1.weak =? f2.weak &&
+            f1.hnf =? f2.hnf &&
+            f1.primops =? f2.primops &&
+            f1.do_not_unfold_pure_lets =? f2.do_not_unfold_pure_lets &&
+            f1.unfold_until =? f2.unfold_until &&
+            f1.unfold_only =? f2.unfold_only &&
+            f1.unfold_fully =? f2.unfold_fully &&
+            f1.unfold_attr =? f2.unfold_attr &&
+            f1.unfold_qual =? f2.unfold_qual &&
+            f1.unfold_namespace =? f2.unfold_namespace &&
+            f1.unfold_tac =? f2.unfold_tac &&
+            f1.pure_subterms_within_computations =? f2.pure_subterms_within_computations &&
+            f1.simplify =? f2.simplify &&
+            f1.erase_universes =? f2.erase_universes &&
+            f1.allow_unbound_universes =? f2.allow_unbound_universes &&
+            f1.reify_ =? f2.reify_ &&
+            f1.compress_uvars =? f2.compress_uvars &&
+            f1.no_full_norm =? f2.no_full_norm &&
+            f1.check_no_uvars =? f2.check_no_uvars &&
+            f1.unmeta =? f2.unmeta &&
+            f1.unascribe =? f2.unascribe &&
+            f1.in_full_norm_request =? f2.in_full_norm_request &&
+            f1.weakly_reduce_scrutinee =? f2.weakly_reduce_scrutinee &&
+            f1.nbe_step =? f2.nbe_step &&
+            f1.for_extraction =? f2.for_extraction &&
+            f1.unrefine =? f2.unrefine &&
+            f1.default_univs_to_zero =? f2.default_univs_to_zero);
+}
+
 let default_steps : fsteps = {
     beta = true;
     iota = true;
@@ -416,7 +451,7 @@ let translate_norm_step = function
 
 let translate_norm_steps s =
     let s = List.concatMap translate_norm_step s in
-    let add_exclude s z = if BU.for_some (eq_step z) s then s else Exclude z :: s in
+    let add_exclude s z = if BU.for_some ((=?) z) s then s else Exclude z :: s in
     let s = Beta::s in
     let s = add_exclude s Zeta in
     let s = add_exclude s Iota in
diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fsti b/src/typechecker/FStar.TypeChecker.Cfg.fsti
index 4002c69abc1..d5683f2f060 100644
--- a/src/typechecker/FStar.TypeChecker.Cfg.fsti
+++ b/src/typechecker/FStar.TypeChecker.Cfg.fsti
@@ -32,6 +32,7 @@ open FStar.TypeChecker.Env
 open FStar.TypeChecker.Primops
 
 open FStar.Class.Show
+open FStar.Class.Deq
 
 module S  = FStar.Syntax.Syntax
 module SS = FStar.Syntax.Subst
@@ -78,6 +79,8 @@ type fsteps = {
      default_univs_to_zero:bool; (* Default unresolved universe levels to zero *)
 }
 
+instance val deq_fsteps : deq fsteps
+
 val default_steps : fsteps
 val fstep_add_one : step -> fsteps -> fsteps
 val to_fsteps : list step -> fsteps
@@ -105,7 +108,7 @@ type cfg = {
      delta_level: list Env.delta_level;  // Controls how much unfolding of definitions should be performed
      primitive_steps:BU.psmap primitive_step;
      strong : bool;                       // under a binder
-     memoize_lazy : bool;
+     memoize_lazy : bool;     (* What exactly is this? Seems to be always true now. *)
      normalize_pure_lets: bool;
      reifying : bool;
      compat_memo_ignore_cfg:bool; (* See #2155, #2161, #2986 *)
diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst
index c89ba0dd188..231551b2d57 100644
--- a/src/typechecker/FStar.TypeChecker.Env.fst
+++ b/src/typechecker/FStar.TypeChecker.Env.fst
@@ -71,12 +71,24 @@ let rec eq_step s1 s2 =
   | UnfoldUntil s1, UnfoldUntil s2 -> s1 = s2
   | UnfoldOnly lids1, UnfoldOnly lids2
   | UnfoldFully lids1, UnfoldFully lids2
-  | UnfoldAttr lids1, UnfoldAttr lids2 ->
-      List.length lids1 = List.length lids2 && List.forall2 Ident.lid_equals lids1 lids2
-  | UnfoldQual strs1, UnfoldQual strs2 -> strs1 = strs2
-  | UnfoldNamespace strs1, UnfoldNamespace strs2 -> strs1 = strs2  
+  | UnfoldAttr lids1, UnfoldAttr lids2 -> lids1 =? lids2
+  | UnfoldQual strs1, UnfoldQual strs2 -> strs1 =? strs2
+  | UnfoldNamespace strs1, UnfoldNamespace strs2 -> strs1 =? strs2
   | _ -> false
 
+instance deq_step : deq step = {
+  (=?) = eq_step;
+}
+
+instance deq_delta_level : deq delta_level = {
+  (=?) = (fun x y -> match x, y with
+    | NoDelta, NoDelta -> true
+    | InliningDelta, InliningDelta -> true
+    | Eager_unfolding_only, Eager_unfolding_only -> true
+    | Unfold x, Unfold y -> x =? y
+    | _ -> false);
+}
+
 let preprocess env tau tm  = env.mpreprocess env tau tm
 let postprocess env tau ty tm = env.postprocess env tau ty tm
 
diff --git a/src/typechecker/FStar.TypeChecker.Env.fsti b/src/typechecker/FStar.TypeChecker.Env.fsti
index 45013b59836..359b515c8f0 100644
--- a/src/typechecker/FStar.TypeChecker.Env.fsti
+++ b/src/typechecker/FStar.TypeChecker.Env.fsti
@@ -22,6 +22,7 @@ open FStar.Syntax.Syntax
 open FStar.Ident
 open FStar.TypeChecker.Common
 open FStar.Class.Binders
+open FStar.Class.Deq
 
 module BU = FStar.Compiler.Util
 module S = FStar.Syntax.Syntax
@@ -63,7 +64,7 @@ type step =
   | DefaultUnivsToZero // default al unresolved universe uvars to zero
 and steps = list step
 
-val eq_step : step -> step -> bool
+instance val deq_step : deq step
 
 type sig_binding = list lident * sigelt
 
@@ -73,6 +74,8 @@ type delta_level =
   | Eager_unfolding_only
   | Unfold of delta_depth
 
+instance val deq_delta_level : deq delta_level
+
 // A name prefix, such as ["FStar";"Math"]
 type name_prefix = FStar.Ident.path
 // A choice of which name prefixes are enabled/disabled
diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst
index e62452e4b86..73f82e61254 100644
--- a/src/typechecker/FStar.TypeChecker.Normalize.fst
+++ b/src/typechecker/FStar.TypeChecker.Normalize.fst
@@ -36,6 +36,7 @@ open FStar.TypeChecker.Env
 open FStar.TypeChecker.Cfg
 
 open FStar.Class.Show
+open FStar.Class.Deq
 
 module S  = FStar.Syntax.Syntax
 module SS = FStar.Syntax.Subst
@@ -117,11 +118,17 @@ type stack = list stack_elt
 
 let head_of t = let hd, _ = U.head_and_args_full t in hd
 
+(* Decides whether a memo taken in config c1 is valid when reducing in config c2. *)
+let cfg_equivalent (c1 c2 : Cfg.cfg) : bool =
+  c1.steps =? c2.steps &&
+  c1.delta_level =? c2.delta_level &&
+  c1.normalize_pure_lets =? c2.normalize_pure_lets
+
 let read_memo cfg (r:memo (Cfg.cfg * 'a)) : option 'a =
   match !r with
   (* We only take this memoized value if the cfg matches the current
   one, or if we are running in compatibility mode for it. *)
-  | Some (cfg', a) when cfg.compat_memo_ignore_cfg || BU.physical_equality cfg cfg' ->
+  | Some (cfg', a) when cfg.compat_memo_ignore_cfg || BU.physical_equality cfg cfg' || cfg_equivalent cfg' cfg ->
     Some a
   | _ -> None
 
@@ -791,7 +798,7 @@ let rejig_norm_request (hd:term) (args:args) :term =
      | _ -> failwith "Impossible! invalid rejig_norm_request for norm")
   | _ -> failwith ("Impossible! invalid rejig_norm_request for: %s" ^ (Print.term_to_string hd))
 
-let is_nbe_request s = BU.for_some (eq_step NBE) s
+let is_nbe_request s = BU.for_some ((=?) NBE) s
 
 let get_norm_request cfg (full_norm:term -> term) args =
     let parse_steps s =
diff --git a/tests/bug-reports/Bug2155.fst b/tests/bug-reports/Bug2155.fst
index 5659e39978e..ff5cd33bacb 100644
--- a/tests/bug-reports/Bug2155.fst
+++ b/tests/bug-reports/Bug2155.fst
@@ -8,6 +8,6 @@ let _ = assert True by begin
   let t = `(f (100 + 100)) in
   let t = norm_term [delta] t in
   (* dump (term_to_string t); *)
-  guard (term_eq t (`(Cons #int 200 (Cons #int (100+100) (Nil #int)))));
+  guard (term_eq t (`(Cons u#0 #int 200 (Cons u#0 #int (100+100) (Nil u#0 #int)))));
   ()
 end
diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile
index 8b59a75992c..426ebce83ea 100644
--- a/tests/bug-reports/Makefile
+++ b/tests/bug-reports/Makefile
@@ -55,7 +55,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug
   Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \
   Bug2415.fst Bug3028.fst Bug2954.fst Bug3089.fst Bug3102.fst Bug2981.fst Bug2980.fst Bug3115.fst \
   Bug2083.fst Bug2002.fst Bug1482.fst Bug1066.fst Bug3120a.fst Bug3120b.fst Bug3186.fst Bug3185.fst Bug3210.fst \
-  Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst
+  Bug3213.fst Bug3213b.fst Bug3207.fst Bug3207b.fst Bug3207c.fst Bug2155.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst
diff --git a/tests/error-messages/Bug3102.fst.expected b/tests/error-messages/Bug3102.fst.expected
index 3f202be8e04..23623554f05 100644
--- a/tests/error-messages/Bug3102.fst.expected
+++ b/tests/error-messages/Bug3102.fst.expected
@@ -16,19 +16,19 @@
 >>]
 >> Got issues: [
 * Error 56 at Bug3102.fst(33,29-35,27):
-  - Bound variable 'e2#1057' would escape in the type of this letbinding
+  - Bound variable 'e2#1041' would escape in the type of this letbinding
   - Add a type annotation that does not mention it
 
 >>]
 >> Got issues: [
 * Error 56 at Bug3102.fst(41,16-43,8):
-  - Bound variable 'z#1176' would escape in the type of this letbinding
+  - Bound variable 'z#1160' would escape in the type of this letbinding
   - Add a type annotation that does not mention it
 
 >>]
 >> Got issues: [
 * Error 56 at Bug3102.fst(49,16-51,7):
-  - Bound variable 'z#1259' would escape in the type of this letbinding
+  - Bound variable 'z#1243' would escape in the type of this letbinding
   - Add a type annotation that does not mention it
 
 >>]
diff --git a/tests/micro-benchmarks/NormCfgMemo.fst b/tests/micro-benchmarks/NormCfgMemo.fst
new file mode 100644
index 00000000000..7063c216cf5
--- /dev/null
+++ b/tests/micro-benchmarks/NormCfgMemo.fst
@@ -0,0 +1,9 @@
+module NormCfgMemo
+
+let rec countdown (n:nat) : bool =
+  if n = 0 then true else countdown (n-1)
+
+(* This should be very quick, it takes ~140ms in my current
+setup. Before fixing the cfg check in Normalizer.read_memo,
+this would take much longer, possibly hours. *)
+let _ = assert_norm (countdown 20000)