Merge pull request #3526 from mtzguido/nits

Nits
FStarLang · Oct 5, 2024 · 2acf23c · 2acf23c
2 parents 0a9b58b + 1b38d86
commit 2acf23c
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 4 deletions.
diff --git 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
diff --git 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} ->