diff --git a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
index 10006c2add0..39a2a8d8a6f 100644
--- a/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
+++ b/ocaml/fstar-lib/generated/FStar_Parser_Const.ml
@@ -296,6 +296,8 @@ let (deprecated_attr : FStar_Ident.lident) = pconst "deprecated"
 let (warn_on_use_attr : FStar_Ident.lident) = pconst "warn_on_use"
 let (inline_let_attr : FStar_Ident.lident) =
   p2l ["FStar"; "Pervasives"; "inline_let"]
+let (no_inline_let_attr : FStar_Ident.lident) =
+  p2l ["FStar"; "Pervasives"; "no_inline_let"]
 let (rename_let_attr : FStar_Ident.lident) =
   p2l ["FStar"; "Pervasives"; "rename_let"]
 let (plugin_attr : FStar_Ident.lident) =
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
index 988ceab41f7..b8b6ba650f7 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Util.ml
@@ -2041,6 +2041,8 @@ let (tcdecltime_attr : FStar_Syntax_Syntax.term) =
   fvar_const FStar_Parser_Const.tcdecltime_attr
 let (inline_let_attr : FStar_Syntax_Syntax.term) =
   fvar_const FStar_Parser_Const.inline_let_attr
+let (no_inline_let_attr : FStar_Syntax_Syntax.term) =
+  fvar_const FStar_Parser_Const.no_inline_let_attr
 let (rename_let_attr : FStar_Syntax_Syntax.term) =
   fvar_const FStar_Parser_Const.rename_let_attr
 let (t_ctx_uvar_and_sust : FStar_Syntax_Syntax.term) =
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
index 419a7b38b81..34e61e68ce7 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Cfg.ml
@@ -2631,21 +2631,27 @@ let (should_reduce_local_let :
          if uu___1
          then true
          else
-           (let n =
-              FStar_TypeChecker_Env.norm_eff_name cfg1.tcenv
-                lb.FStar_Syntax_Syntax.lbeff in
-            let uu___3 =
-              (FStar_Syntax_Util.is_pure_effect n) &&
-                (cfg1.normalize_pure_lets ||
-                   (FStar_Syntax_Util.has_attribute
-                      lb.FStar_Syntax_Syntax.lbattrs
-                      FStar_Parser_Const.inline_let_attr)) in
+           (let uu___3 =
+              FStar_Syntax_Util.has_attribute lb.FStar_Syntax_Syntax.lbattrs
+                FStar_Parser_Const.no_inline_let_attr in
             if uu___3
-            then true
+            then false
             else
-              (FStar_Syntax_Util.is_ghost_effect n) &&
-                (Prims.op_Negation
-                   (cfg1.steps).pure_subterms_within_computations)))
+              (let n =
+                 FStar_TypeChecker_Env.norm_eff_name cfg1.tcenv
+                   lb.FStar_Syntax_Syntax.lbeff in
+               let uu___5 =
+                 (FStar_Syntax_Util.is_pure_effect n) &&
+                   (cfg1.normalize_pure_lets ||
+                      (FStar_Syntax_Util.has_attribute
+                         lb.FStar_Syntax_Syntax.lbattrs
+                         FStar_Parser_Const.inline_let_attr)) in
+               if uu___5
+               then true
+               else
+                 (FStar_Syntax_Util.is_ghost_effect n) &&
+                   (Prims.op_Negation
+                      (cfg1.steps).pure_subterms_within_computations))))
 let (translate_norm_step :
   FStar_Pervasives.norm_step -> FStar_TypeChecker_Env.step Prims.list) =
   fun uu___ ->
diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst
index a091a3d7748..5a808691293 100644
--- a/src/parser/FStar.Parser.Const.fst
+++ b/src/parser/FStar.Parser.Const.fst
@@ -352,6 +352,7 @@ let steps_unmeta        = psconst "unmeta"
 let deprecated_attr = pconst "deprecated"
 let warn_on_use_attr = pconst "warn_on_use"
 let inline_let_attr = p2l ["FStar"; "Pervasives"; "inline_let"]
+let no_inline_let_attr = p2l ["FStar"; "Pervasives"; "no_inline_let"]
 let rename_let_attr = p2l ["FStar"; "Pervasives"; "rename_let"]
 let plugin_attr     = p2l ["FStar"; "Pervasives"; "plugin"]
 let tcnorm_attr    =  p2l ["FStar"; "Pervasives"; "tcnorm"]
diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst
index bed2bb7ab33..26df4cb0420 100644
--- a/src/syntax/FStar.Syntax.Util.fst
+++ b/src/syntax/FStar.Syntax.Util.fst
@@ -1008,6 +1008,7 @@ let tac_opaque_attr = exp_string "tac_opaque"
 let dm4f_bind_range_attr = fvar_const PC.dm4f_bind_range_attr
 let tcdecltime_attr = fvar_const PC.tcdecltime_attr
 let inline_let_attr = fvar_const PC.inline_let_attr
+let no_inline_let_attr = fvar_const PC.no_inline_let_attr
 let rename_let_attr = fvar_const PC.rename_let_attr
 
 let t_ctx_uvar_and_sust = fvar_const PC.ctx_uvar_and_subst_lid
diff --git a/src/typechecker/FStar.TypeChecker.Cfg.fst b/src/typechecker/FStar.TypeChecker.Cfg.fst
index c1f4ea95f70..08f5730cbbe 100644
--- a/src/typechecker/FStar.TypeChecker.Cfg.fst
+++ b/src/typechecker/FStar.TypeChecker.Cfg.fst
@@ -431,13 +431,15 @@ let should_reduce_local_let cfg lb =
   else if cfg.steps.pure_subterms_within_computations &&
           U.has_attribute lb.lbattrs PC.inline_let_attr
   then true //1. we're extracting, and it's marked @inline_let
+  else if U.has_attribute lb.lbattrs PC.no_inline_let_attr
+  then false //Or, 2. do not unfold as it's explicitly marked as @no_inline_let
   else
     let n = Env.norm_eff_name cfg.tcenv lb.lbeff in
     if U.is_pure_effect n &&
        (cfg.normalize_pure_lets
         || U.has_attribute lb.lbattrs PC.inline_let_attr)
-    then true //Or, 2. it's pure and we either not extracting, or it's marked @inline_let
-    else U.is_ghost_effect n && //Or, 3. it's ghost and we're not extracting
+    then true //Or, 3. it's pure and we are either not extracting, or it's marked @inline_let
+    else U.is_ghost_effect n && //Or, 4. it's ghost and we're not extracting
          not (cfg.steps.pure_subterms_within_computations)
 
 let translate_norm_step = function
diff --git a/tests/extraction/Makefile b/tests/extraction/Makefile
index 84952c9372c..c7b546a16df 100644
--- a/tests/extraction/Makefile
+++ b/tests/extraction/Makefile
@@ -2,7 +2,7 @@ FSTAR_EXAMPLES=$(realpath ../../examples)
 include $(FSTAR_EXAMPLES)/Makefile.include
 include $(FSTAR_ULIB)/ml/Makefile.include
 
-all: inline_let all_cmi Eta_expand.test Div.test
+all: inline_let all_cmi Eta_expand.test Div.test no_inline_let
 
 %.exe: %.fst | out
 	$(FSTAR) $(FSTAR_DEFAULT_ARGS) --odir out --codegen OCaml $<
@@ -25,6 +25,11 @@ inline_let: InlineLet.fst
 	egrep -A 10 test InlineLet.ml | grep -qs "17"
 	@touch $@
 
+no_inline_let: NoInlineLet.fst
+	$(FSTAR) --codegen OCaml NoInlineLet.fst
+	diff -u --strip-trailing-cr NoInlineLet.ml.expected NoInlineLet.ml
+	@touch $@
+
 all_cmi:
 	+$(MAKE) -C cmi all
 
diff --git a/tests/extraction/NoInlineLet.fst b/tests/extraction/NoInlineLet.fst
new file mode 100644
index 00000000000..48d0c90996a
--- /dev/null
+++ b/tests/extraction/NoInlineLet.fst
@@ -0,0 +1,15 @@
+module NoInlineLet
+open FStar.Tactics
+
+let test_no_inline (f: int): int =
+  (* this one shouldn't be inlined in tactics or extraction *)
+  [@@no_inline_let]
+  let x = f + 1 in
+  (* this one will be inlined by the norm tactic in the below test *)
+  let y = x + 2 in
+  y + y
+
+[@@(postprocess_with (fun _ -> norm [delta_only [`%test_no_inline]]; trefl ()))]
+let test_postprocess (f: int): int =
+  let x = test_no_inline f in
+  x
diff --git a/tests/extraction/NoInlineLet.ml.expected b/tests/extraction/NoInlineLet.ml.expected
new file mode 100644
index 00000000000..ea507f656af
--- /dev/null
+++ b/tests/extraction/NoInlineLet.ml.expected
@@ -0,0 +1,8 @@
+open Prims
+let (test_no_inline : Prims.int -> Prims.int) =
+  fun f ->
+    let x = f + Prims.int_one in let y = x + (Prims.of_int (2)) in y + y
+let (test_postprocess : Prims.int -> Prims.int) =
+  fun f ->
+    let x = f + Prims.int_one in
+    (x + (Prims.of_int (2))) + (x + (Prims.of_int (2)))
\ No newline at end of file
diff --git a/ulib/FStar.Pervasives.fst b/ulib/FStar.Pervasives.fst
index 42987e0cdc6..5d6c1e8eccd 100644
--- a/ulib/FStar.Pervasives.fst
+++ b/ulib/FStar.Pervasives.fst
@@ -141,6 +141,8 @@ let rec false_elim #_ _ = false_elim ()
 
 let inline_let = ()
 
+let no_inline_let = ()
+
 let rename_let _ = ()
 
 let plugin _ = ()
diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti
index 6bb8b1076a3..d1288d56c9b 100644
--- a/ulib/FStar.Pervasives.fsti
+++ b/ulib/FStar.Pervasives.fsti
@@ -847,6 +847,12 @@ type __internal_ocaml_attributes =
     size. *)
 val inline_let : unit
 
+(** The [no_inline_let] attribute on a local let-binding prevents the
+    normalizer from unfolding the definition of a local let-binding. This
+    attribute can be useful when processing definitions with tactics, as
+    otherwise the normalizer will eagerly unfold all pure definitions. *)
+val no_inline_let : unit
+
 (** The [rename_let] attribute support a form of metaprogramming for
     the names of let-bound variables used in extracted code.