diff --git a/ocaml/fstar-lib/FStar_Tactics_Load.ml b/ocaml/fstar-lib/FStar_Tactics_Load.ml
index aeee4e835c3..c22edf02074 100644
--- a/ocaml/fstar-lib/FStar_Tactics_Load.ml
+++ b/ocaml/fstar-lib/FStar_Tactics_Load.ml
@@ -6,12 +6,14 @@ module EC = FStar_Errors_Codes
 module EM = FStar_Errors_Msg
 module O = FStar_Options
 
+let pout  s   = if FStar_Compiler_Debug.any () then U.print_string s
+let pout1 s x = if FStar_Compiler_Debug.any () then U.print1 s x
 let perr  s   = if FStar_Compiler_Debug.any () then U.print_error s
 let perr1 s x = if FStar_Compiler_Debug.any () then U.print1_error s x
 
 let dynlink (fname:string) : unit =
   try
-    perr ("Attempting to load " ^ fname ^ "\n");
+    pout ("Attempting to load " ^ fname ^ "\n");
     Dynlink.loadfile fname
   with Dynlink.Error e ->
     E.log_issue_doc FStar_Compiler_Range.dummyRange EC.Error_PluginDynlink [
@@ -25,7 +27,7 @@ let dynlink (fname:string) : unit =
 
 let load_tactic tac =
   dynlink tac;
-  perr1 "Loaded %s\n" tac
+  pout1 "Loaded %s\n" tac
 
 let load_tactics tacs =
     List.iter load_tactic tacs
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
index 5fa1cbe3830..d91781037a5 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Core.ml
@@ -5270,7 +5270,14 @@ and (do_check :
                                   Success uu___6
                               | err -> err)
                          | Error err -> Error err)
-                    else fail "Let binding is effectful"))
+                    else
+                      (let uu___4 =
+                         let uu___5 =
+                           FStar_Class_Show.show FStar_Ident.showable_lident
+                             lb.FStar_Syntax_Syntax.lbeff in
+                         FStar_Compiler_Util.format1
+                           "Let binding is effectful (lbeff = %s)" uu___5 in
+                       fail uu___4)))
       | FStar_Syntax_Syntax.Tm_match
           { FStar_Syntax_Syntax.scrutinee = sc;
             FStar_Syntax_Syntax.ret_opt = FStar_Pervasives_Native.None;
diff --git a/src/typechecker/FStar.TypeChecker.Core.fst b/src/typechecker/FStar.TypeChecker.Core.fst
index 35dc2b1b7ba..b85c39de4a7 100644
--- a/src/typechecker/FStar.TypeChecker.Core.fst
+++ b/src/typechecker/FStar.TypeChecker.Core.fst
@@ -1413,7 +1413,7 @@ and do_check (g:env) (e:term)
       )
     )
     else (
-      fail "Let binding is effectful"
+      fail (format1 "Let binding is effectful (lbeff = %s)" (show lb.lbeff))
     )
 
   | Tm_match {scrutinee=sc; ret_opt=None; brs=branches; rc_opt} ->