diff --git a/ocaml/fstar-lib/generated/FStar_Errors.ml b/ocaml/fstar-lib/generated/FStar_Errors.ml
index 37de2fb6699..8d31b47d779 100644
--- a/ocaml/fstar-lib/generated/FStar_Errors.ml
+++ b/ocaml/fstar-lib/generated/FStar_Errors.ml
@@ -391,7 +391,10 @@ let (format_issue' : Prims.bool -> issue -> Prims.string) =
         | uu___ -> FStar_Pprint.empty in
       let mainmsg =
         let uu___ =
-          FStar_Compiler_List.map FStar_Errors_Msg.subdoc issue1.issue_msg in
+          FStar_Compiler_List.map
+            (fun d ->
+               let uu___1 = FStar_Pprint.group d in
+               FStar_Errors_Msg.subdoc uu___1) issue1.issue_msg in
         FStar_Pprint.concat uu___ in
       let doc =
         let uu___ =
@@ -721,7 +724,7 @@ let (set_option_warning_callback_range :
   FStar_Compiler_Range_Type.range FStar_Pervasives_Native.option -> unit) =
   fun ropt ->
     FStar_Options.set_option_warning_callback (warn_unsafe_options ropt)
-let (uu___376 :
+let (uu___377 :
   (((Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) *
     (unit -> FStar_Errors_Codes.error_setting Prims.list)))
   =
@@ -767,10 +770,10 @@ let (uu___376 :
   (set_callbacks, get_error_flags)
 let (t_set_parse_warn_error :
   (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) =
-  match uu___376 with
+  match uu___377 with
   | (t_set_parse_warn_error1, error_flags) -> t_set_parse_warn_error1
 let (error_flags : unit -> FStar_Errors_Codes.error_setting Prims.list) =
-  match uu___376 with
+  match uu___377 with
   | (t_set_parse_warn_error1, error_flags1) -> error_flags1
 let (set_parse_warn_error :
   (Prims.string -> FStar_Errors_Codes.error_setting Prims.list) -> unit) =
diff --git a/ocaml/fstar-lib/generated/FStar_Errors_Msg.ml b/ocaml/fstar-lib/generated/FStar_Errors_Msg.ml
index 09fae5ad74a..083e4f3fdc1 100644
--- a/ocaml/fstar-lib/generated/FStar_Errors_Msg.ml
+++ b/ocaml/fstar-lib/generated/FStar_Errors_Msg.ml
@@ -58,6 +58,8 @@ let (subdoc : FStar_Pprint.document -> FStar_Pprint.document) =
 let (rendermsg : error_message -> Prims.string) =
   fun ds ->
     let uu___ =
-      let uu___1 = FStar_Compiler_List.map subdoc ds in
+      let uu___1 =
+        FStar_Compiler_List.map
+          (fun d -> let uu___2 = FStar_Pprint.group d in subdoc uu___2) ds in
       FStar_Pprint.concat uu___1 in
     renderdoc uu___
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_ErrorReporting.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_ErrorReporting.ml
index 9739d24f10e..3bc63d94d93 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_ErrorReporting.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_ErrorReporting.ml
@@ -139,7 +139,7 @@ let (label_goals :
               | FStar_SMTEncoding_Term.Real uu___1 -> (labels1, q1)
               | FStar_SMTEncoding_Term.LblPos uu___1 -> failwith "Impossible"
               | FStar_SMTEncoding_Term.Labeled
-                  (arg, "could not prove post-condition", label_range) ->
+                  (arg, "Could not prove post-condition", label_range) ->
                   let fallback debug_msg =
                     aux default_msg
                       (FStar_Pervasives_Native.Some label_range)
@@ -237,7 +237,7 @@ let (label_goals :
                                                       then
                                                         let uu___8 =
                                                           aux
-                                                            "could not prove post-condition"
+                                                            "Could not prove post-condition"
                                                             FStar_Pervasives_Native.None
                                                             (FStar_Pervasives_Native.Some
                                                                post_name)
diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
index cec010dc693..2eabd49e3a4 100644
--- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
+++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Solver.ml
@@ -2171,11 +2171,15 @@ let (solve :
           let uu___1 =
             let uu___2 =
               let uu___3 =
-                let uu___4 = FStar_Syntax_Print.term_to_string q in
-                FStar_Compiler_Util.format1
-                  "Q = %s\nA query could not be solved internally, and --no_smt was given"
-                  uu___4 in
-              FStar_Compiler_Effect.op_Less_Bar FStar_Errors_Msg.mkmsg uu___3 in
+                FStar_Errors_Msg.text
+                  "A query could not be solved internally, and --no_smt was given." in
+              let uu___4 =
+                let uu___5 =
+                  let uu___6 = FStar_Errors_Msg.text "Query = " in
+                  let uu___7 = FStar_Syntax_Print_Pretty.term_to_doc q in
+                  FStar_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in
+                [uu___5] in
+              uu___3 :: uu___4 in
             (FStar_Errors_Codes.Error_NoSMTButNeeded, uu___2) in
           FStar_TypeChecker_Err.log_issue tcenv
             tcenv.FStar_TypeChecker_Env.range uu___1
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml
index 2e1848f62af..34086e09d38 100644
--- a/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml
+++ b/ocaml/fstar-lib/generated/FStar_Syntax_Print.ml
@@ -1940,4 +1940,21 @@ let (fv_qual_to_string : FStar_Syntax_Syntax.fv_qual -> Prims.string) =
     | FStar_Syntax_Syntax.Unresolved_projector uu___ ->
         "Unresolved_projector _"
     | FStar_Syntax_Syntax.Unresolved_constructor uu___ ->
-        "Unresolved_constructor _"
\ No newline at end of file
+        "Unresolved_constructor _"
+let (term_to_doc' :
+  FStar_Syntax_DsEnv.env -> FStar_Syntax_Syntax.term -> FStar_Pprint.document)
+  =
+  fun dsenv ->
+    fun t ->
+      let uu___ = FStar_Options.ugly () in
+      if uu___
+      then
+        let uu___1 = term_to_string t in FStar_Pprint.arbitrary_string uu___1
+      else FStar_Syntax_Print_Pretty.term_to_doc' dsenv t
+let (term_to_doc : FStar_Syntax_Syntax.term -> FStar_Pprint.document) =
+  fun t ->
+    let uu___ = FStar_Options.ugly () in
+    if uu___
+    then
+      let uu___1 = term_to_string t in FStar_Pprint.arbitrary_string uu___1
+    else FStar_Syntax_Print_Pretty.term_to_doc t
\ No newline at end of file
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
index f8ff46893ec..0f4b7921656 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Env.ml
@@ -4613,22 +4613,64 @@ let (def_check_vars_in_set :
               Prims.op_Negation uu___2 in
             (if uu___1
              then
+               let doclist ds =
+                 let uu___2 = FStar_Pprint.doc_of_string "[]" in
+                 let uu___3 =
+                   let uu___4 = FStar_Pprint.break_ Prims.int_one in
+                   FStar_Pprint.op_Hat_Hat FStar_Pprint.semi uu___4 in
+                 FStar_Pprint.surround_separate (Prims.of_int (2))
+                   Prims.int_zero uu___2 FStar_Pprint.lbracket uu___3
+                   FStar_Pprint.rbracket ds in
                let uu___2 =
                  let uu___3 =
-                   let uu___4 = FStar_Syntax_Print.term_to_string t in
+                   let uu___4 =
+                     let uu___5 =
+                       FStar_Errors_Msg.text
+                         "Internal: term is not well-scoped " in
+                     let uu___6 =
+                       let uu___7 = FStar_Pprint.doc_of_string msg in
+                       FStar_Pprint.parens uu___7 in
+                     FStar_Pprint.op_Hat_Slash_Hat uu___5 uu___6 in
                    let uu___5 =
-                     let uu___6 = FStar_Compiler_Util.set_elements s in
-                     FStar_Compiler_Effect.op_Bar_Greater uu___6
-                       (FStar_Syntax_Print.bvs_to_string ",\n\t") in
-                   let uu___6 =
-                     let uu___7 = FStar_Compiler_Util.set_elements vset in
-                     FStar_Compiler_Effect.op_Bar_Greater uu___7
-                       (FStar_Syntax_Print.bvs_to_string ",") in
-                   FStar_Compiler_Util.format4
-                     "Internal: term is not closed (%s).\nt = (%s)\nFVs = (%s)\nScope = (%s)\n"
-                     msg uu___4 uu___5 uu___6 in
+                     let uu___6 =
+                       let uu___7 = FStar_Errors_Msg.text "t = " in
+                       let uu___8 = FStar_Syntax_Print.term_to_doc t in
+                       FStar_Pprint.op_Hat_Slash_Hat uu___7 uu___8 in
+                     let uu___7 =
+                       let uu___8 =
+                         let uu___9 = FStar_Errors_Msg.text "FVs = " in
+                         let uu___10 =
+                           let uu___11 =
+                             let uu___12 = FStar_Compiler_Util.set_elements s in
+                             FStar_Compiler_Effect.op_Bar_Greater uu___12
+                               (FStar_Compiler_List.map
+                                  (fun b ->
+                                     let uu___13 =
+                                       FStar_Syntax_Print.bv_to_string b in
+                                     FStar_Pprint.arbitrary_string uu___13)) in
+                           doclist uu___11 in
+                         FStar_Pprint.op_Hat_Slash_Hat uu___9 uu___10 in
+                       let uu___9 =
+                         let uu___10 =
+                           let uu___11 = FStar_Errors_Msg.text "Scope = " in
+                           let uu___12 =
+                             let uu___13 =
+                               let uu___14 =
+                                 FStar_Compiler_Util.set_elements vset in
+                               FStar_Compiler_Effect.op_Bar_Greater uu___14
+                                 (FStar_Compiler_List.map
+                                    (fun b ->
+                                       let uu___15 =
+                                         FStar_Syntax_Print.bv_to_string b in
+                                       FStar_Pprint.arbitrary_string uu___15)) in
+                             doclist uu___13 in
+                           FStar_Pprint.op_Hat_Slash_Hat uu___11 uu___12 in
+                         [uu___10] in
+                       uu___8 :: uu___9 in
+                     uu___6 :: uu___7 in
+                   uu___4 :: uu___5 in
                  (FStar_Errors_Codes.Warning_Defensive, uu___3) in
-               FStar_Errors.log_issue rng uu___2
+               FStar_Errors.log_issue_doc rng uu___2
              else ())
           else ()
 let (def_check_closed_in :
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml
index f23e865f9c7..cc3f2eef178 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_Err.ml
@@ -301,30 +301,20 @@ let (expected_expression_of_type :
           let uu___ =
             let uu___1 =
               let uu___2 =
-                FStar_Pprint.doc_of_string "Expected expression of type" in
+                let uu___3 =
+                  FStar_Errors_Msg.text "Expected expression of type" in
+                FStar_Pprint.prefix (Prims.of_int (4)) Prims.int_one uu___3
+                  d1 in
               let uu___3 =
-                let uu___4 = FStar_Pprint.blank (Prims.of_int (4)) in
+                let uu___4 =
+                  let uu___5 = FStar_Errors_Msg.text "got expression" in
+                  FStar_Pprint.prefix (Prims.of_int (4)) Prims.int_one uu___5
+                    ed in
                 let uu___5 =
-                  let uu___6 = FStar_Pprint.align d1 in
-                  let uu___7 =
-                    let uu___8 = FStar_Pprint.doc_of_string "got expression" in
-                    let uu___9 =
-                      let uu___10 = FStar_Pprint.blank (Prims.of_int (4)) in
-                      let uu___11 =
-                        let uu___12 = FStar_Pprint.align ed in
-                        let uu___13 =
-                          let uu___14 = FStar_Pprint.doc_of_string "of type" in
-                          let uu___15 =
-                            let uu___16 =
-                              FStar_Pprint.blank (Prims.of_int (4)) in
-                            let uu___17 = FStar_Pprint.align d2 in
-                            FStar_Pprint.op_Hat_Hat uu___16 uu___17 in
-                          FStar_Pprint.op_Hat_Slash_Hat uu___14 uu___15 in
-                        FStar_Pprint.op_Hat_Slash_Hat uu___12 uu___13 in
-                      FStar_Pprint.op_Hat_Hat uu___10 uu___11 in
-                    FStar_Pprint.op_Hat_Slash_Hat uu___8 uu___9 in
-                  FStar_Pprint.op_Hat_Slash_Hat uu___6 uu___7 in
-                FStar_Pprint.op_Hat_Hat uu___4 uu___5 in
+                  let uu___6 = FStar_Errors_Msg.text "of type" in
+                  FStar_Pprint.prefix (Prims.of_int (4)) Prims.int_one uu___6
+                    d2 in
+                FStar_Pprint.op_Hat_Slash_Hat uu___4 uu___5 in
               FStar_Pprint.op_Hat_Slash_Hat uu___2 uu___3 in
             [uu___1] in
           (FStar_Errors_Codes.Fatal_UnexpectedExpressionType, uu___)
diff --git a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
index e79d773c2cd..4b0a4ef3073 100644
--- a/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
+++ b/ocaml/fstar-lib/generated/FStar_TypeChecker_TcTerm.ml
@@ -747,7 +747,7 @@ let (check_expected_effect :
                                         FStar_TypeChecker_Env.get_range env in
                                       FStar_TypeChecker_Util.label_guard
                                         uu___7
-                                        "could not prove post-condition" g in
+                                        "Could not prove post-condition" g in
                                     ((let uu___8 =
                                         FStar_TypeChecker_Env.debug env
                                           FStar_Options.Medium in
diff --git a/src/basic/FStar.Errors.Msg.fst b/src/basic/FStar.Errors.Msg.fst
index 1d411adc442..becd4bfca42 100644
--- a/src/basic/FStar.Errors.Msg.fst
+++ b/src/basic/FStar.Errors.Msg.fst
@@ -40,4 +40,4 @@ let subdoc d =
   else blank 2 ^^ doc_of_string "-" ^^ blank 1 ^^ align d ^^ hardline
 
 let rendermsg (ds : list document) : string =
-  renderdoc (concat (List.map subdoc ds))
+  renderdoc (concat (List.map (fun d -> subdoc (group d)) ds))
diff --git a/src/basic/FStar.Errors.fst b/src/basic/FStar.Errors.fst
index 2ffd5bce0bb..c1ed3580b33 100644
--- a/src/basic/FStar.Errors.fst
+++ b/src/basic/FStar.Errors.fst
@@ -183,7 +183,7 @@ let format_issue' (print_hdr:bool) (issue:issue) : string =
     | _ -> empty
   in
   let mainmsg : document =
-    concat (List.map subdoc issue.issue_msg)
+    concat (List.map (fun d -> subdoc (group d)) issue.issue_msg)
   in
   let doc : document =
     (* This ends in a hardline to get a 1-line spacing between errors *)
diff --git a/src/smtencoding/FStar.SMTEncoding.ErrorReporting.fst b/src/smtencoding/FStar.SMTEncoding.ErrorReporting.fst
index 376c3088fb3..597c6ce2bdd 100644
--- a/src/smtencoding/FStar.SMTEncoding.ErrorReporting.fst
+++ b/src/smtencoding/FStar.SMTEncoding.ErrorReporting.fst
@@ -114,7 +114,7 @@ let label_goals use_env_msg  //when present, provides an alternate error message
 
         | LblPos _ -> failwith "Impossible" //these get added after errorReporting instrumentation only
 
-        | Labeled(arg, "could not prove post-condition", label_range) ->
+        | Labeled(arg, "Could not prove post-condition", label_range) ->
           //printfn "GOT A LABELED WP IMPLICATION\n\t%s"
           //        (Term.print_smt_term q);
           let fallback debug_msg =
@@ -138,7 +138,7 @@ let label_goals use_env_msg  //when present, provides an alternate error message
                         | Quant(Forall, pats_ens, iopt_ens, sorts_ens, {tm=App(Imp, [ensures_conjuncts; post]); rng=rng_ens}) ->
                           if is_a_post_condition (Some post_name) post
                           then
-                            let labels, ensures_conjuncts = aux "could not prove post-condition" None (Some post_name) labels ensures_conjuncts in
+                            let labels, ensures_conjuncts = aux "Could not prove post-condition" None (Some post_name) labels ensures_conjuncts in
                             let pats_ens =
                               match pats_ens with
                               | []
diff --git a/src/smtencoding/FStar.SMTEncoding.Solver.fst b/src/smtencoding/FStar.SMTEncoding.Solver.fst
index fd453d4c279..b37490b6761 100644
--- a/src/smtencoding/FStar.SMTEncoding.Solver.fst
+++ b/src/smtencoding/FStar.SMTEncoding.Solver.fst
@@ -1262,11 +1262,13 @@ automatically retry increasing fuel as needed, and perform quake testing
 _log_ (not raise) an error if the VC could not be proven. *)
 let solve use_env_msg tcenv q : unit =
     if Options.no_smt () then
+        let open FStar.Errors.Msg in
+        let open FStar.Pprint in
         FStar.TypeChecker.Err.log_issue
           tcenv tcenv.range
             (Errors.Error_NoSMTButNeeded,
-             Errors.mkmsg <|
-             BU.format1 "Q = %s\nA query could not be solved internally, and --no_smt was given" (Print.term_to_string q))
+             [text "A query could not be solved internally, and --no_smt was given.";
+              text "Query = " ^/^ FStar.Syntax.Print.Pretty.term_to_doc q])
     else
     Profiling.profile
       (fun () -> do_solve_maybe_split use_env_msg tcenv q)
diff --git a/src/syntax/FStar.Syntax.Print.fst b/src/syntax/FStar.Syntax.Print.fst
index 4ebbbb7f93b..6a6fc44959f 100644
--- a/src/syntax/FStar.Syntax.Print.fst
+++ b/src/syntax/FStar.Syntax.Print.fst
@@ -935,3 +935,13 @@ let fv_qual_to_string fvq =
   | Record_ctor _ -> "Record_ctor _"
   | Unresolved_projector _ -> "Unresolved_projector _"
   | Unresolved_constructor _ -> "Unresolved_constructor _"
+
+let term_to_doc' dsenv t =
+  if Options.ugly ()
+  then Pprint.arbitrary_string (term_to_string t)
+  else Pretty.term_to_doc' dsenv t
+
+let term_to_doc t =
+  if Options.ugly ()
+  then Pprint.arbitrary_string (term_to_string t)
+  else Pretty.term_to_doc t
diff --git a/src/syntax/FStar.Syntax.Print.fsti b/src/syntax/FStar.Syntax.Print.fsti
index 00093b60e8f..dda5c659da3 100644
--- a/src/syntax/FStar.Syntax.Print.fsti
+++ b/src/syntax/FStar.Syntax.Print.fsti
@@ -79,3 +79,6 @@ val ctx_uvar_to_string_no_reason    : ctx_uvar -> string
 val emb_typ_to_string: emb_typ -> string
 
 val fv_qual_to_string : fv_qual -> string
+
+val term_to_doc'          : DsEnv.env -> term -> Pprint.document
+val term_to_doc           : term -> Pprint.document
diff --git a/src/typechecker/FStar.TypeChecker.Env.fst b/src/typechecker/FStar.TypeChecker.Env.fst
index 1407b9cae3f..b070da0e2c2 100644
--- a/src/typechecker/FStar.TypeChecker.Env.fst
+++ b/src/typechecker/FStar.TypeChecker.Env.fst
@@ -1153,14 +1153,17 @@ let def_check_vars_in_set rng msg vset t =
     if Options.defensive () then begin
         let s = Free.names t in
         if not (BU.set_is_empty <| BU.set_difference s vset)
-        then Errors.log_issue rng
-                    (Errors.Warning_Defensive,
-                     BU.format4 "Internal: term is not closed (%s).\nt = (%s)\nFVs = (%s)\nScope = (%s)\n"
-                                      msg
-                                      (Print.term_to_string t)
-                                      (BU.set_elements s |> Print.bvs_to_string ",\n\t")
-                                      (BU.set_elements vset |> Print.bvs_to_string ",")
-                                      )
+        then 
+          let open FStar.Pprint in
+          let doclist (ds : list Pprint.document) : Pprint.document =
+            surround_separate 2 0 (doc_of_string "[]") lbracket (semi ^^ break_ 1) rbracket ds
+          in
+          Errors.log_issue_doc rng (Errors.Warning_Defensive, [
+               text "Internal: term is not well-scoped " ^/^ parens (doc_of_string msg);
+               text "t = " ^/^ Print.term_to_doc t;
+               text "FVs = " ^/^ doclist (BU.set_elements s |> List.map (fun b -> arbitrary_string (Print.bv_to_string b)));
+               text "Scope = " ^/^ doclist (BU.set_elements vset |> List.map (fun b -> arbitrary_string (Print.bv_to_string b)));
+             ])
     end
 
 let def_check_closed_in rng msg l t =
diff --git a/src/typechecker/FStar.TypeChecker.Err.fst b/src/typechecker/FStar.TypeChecker.Err.fst
index acaa7bd6808..c10e0c1ec5e 100644
--- a/src/typechecker/FStar.TypeChecker.Err.fst
+++ b/src/typechecker/FStar.TypeChecker.Err.fst
@@ -205,15 +205,12 @@ let expected_expression_of_type env t1 e t2 =
   let d1 = N.term_to_doc env t1 in
   let d2 = N.term_to_doc env t2 in
   let ed = N.term_to_doc env e in
-  let open FStar.Pprint in
-  (Errors.Fatal_UnexpectedExpressionType,
-    [doc_of_string "Expected expression of type"
-    ^/^ blank 4 ^^ align d1
-    ^/^ doc_of_string "got expression"
-    ^/^ blank 4 ^^ align ed
-    ^/^ doc_of_string "of type"
-    ^/^ blank 4 ^^ align d2
-    ])
+  let open FStar.Errors.Msg in
+  (Errors.Fatal_UnexpectedExpressionType, [
+    prefix 4 1 (text "Expected expression of type") d1 ^/^
+    prefix 4 1 (text "got expression") ed ^/^
+    prefix 4 1 (text "of type") d2
+  ])
 
 let expected_pattern_of_type env t1 e t2 =
   let s1, s2 = err_msg_type_strings env t1 t2 in
diff --git a/src/typechecker/FStar.TypeChecker.Rel.fst b/src/typechecker/FStar.TypeChecker.Rel.fst
index 8239b27f85a..3e1188faecb 100644
--- a/src/typechecker/FStar.TypeChecker.Rel.fst
+++ b/src/typechecker/FStar.TypeChecker.Rel.fst
@@ -3690,6 +3690,8 @@ and solve_t' (problem:tprob) (wl:worklist) : solution =
                     | _ -> None
                 in
                 let is_reveal_or_hide t =
+                  // Returns Inl (u, ty, t) for reveal u#u #ty t
+                  // Returns Inr (u, ty, t) for hide u#u #ty t
                   let h, args = U.head_and_args t in
                   if U.is_fvar PC.reveal h
                   then match payload_of_hide_reveal h args with
diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fst b/src/typechecker/FStar.TypeChecker.TcTerm.fst
index cf90221b5e3..285036e682c 100644
--- a/src/typechecker/FStar.TypeChecker.TcTerm.fst
+++ b/src/typechecker/FStar.TypeChecker.TcTerm.fst
@@ -317,7 +317,7 @@ let check_expected_effect env (use_eq:bool) (copt:option comp) (ec : term * comp
                  (Print.comp_to_string expected_c)
                  (string_of_bool use_eq);
        let e, _, g = TcUtil.check_comp env use_eq e c expected_c in
-       let g = TcUtil.label_guard (Env.get_range env) "could not prove post-condition" g in
+       let g = TcUtil.label_guard (Env.get_range env) "Could not prove post-condition" g in
        if debug env Options.Medium
        then BU.print2 "(%s) DONE check_expected_effect;\n\tguard is: %s\n"
                          (Range.string_of_range e.pos)
diff --git a/tests/error-messages/AnotType.fst.expected b/tests/error-messages/AnotType.fst.expected
index d722727a37d..7a74ff49aad 100644
--- a/tests/error-messages/AnotType.fst.expected
+++ b/tests/error-messages/AnotType.fst.expected
@@ -6,12 +6,7 @@
 >>]
 >> Got issues: [
 * Error 189 at AnotType.fst(27,14-27,16):
-  - Expected expression of type
-        Type0
-    got expression
-        tb
-    of type
-        Type
+  - Expected expression of type Type0 got expression tb of type Type
 
 >>]
 Verified module: AnotType
diff --git a/tests/error-messages/Basic.fst.expected b/tests/error-messages/Basic.fst.expected
index 591c4e09fd9..379d8e249a2 100644
--- a/tests/error-messages/Basic.fst.expected
+++ b/tests/error-messages/Basic.fst.expected
@@ -1,11 +1,6 @@
 >> Got issues: [
 * Error 189 at Basic.fst(4,13-4,17):
-  - Expected expression of type
-        Prims.int
-    got expression
-        true
-    of type
-        Prims.bool
+  - Expected expression of type Prims.int got expression true of type Prims.bool
 
 >>]
 >> Got issues: [
diff --git a/tests/error-messages/Bug1988.fst.expected b/tests/error-messages/Bug1988.fst.expected
index 66bc98f2e63..7a4573080b6 100644
--- a/tests/error-messages/Bug1988.fst.expected
+++ b/tests/error-messages/Bug1988.fst.expected
@@ -1,11 +1,8 @@
 >> Got issues: [
 * Error 189 at Bug1988.fst(4,14-4,30):
-  - Expected expression of type
-        Prims.int
-    got expression
-        "string literal"
-    of type
-        Prims.string
+  - Expected expression of type Prims.int
+    got expression "string literal"
+    of type Prims.string
 
 >>]
 >> Got issues: [
diff --git a/tests/error-messages/ExpectFailure.fst.expected b/tests/error-messages/ExpectFailure.fst.expected
index d388fea4643..accb5634609 100644
--- a/tests/error-messages/ExpectFailure.fst.expected
+++ b/tests/error-messages/ExpectFailure.fst.expected
@@ -1,21 +1,15 @@
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(20,12-20,15):
-  - Expected expression of type
-        Prims.int
-    got expression
-        'a'
-    of type
-        FStar.Char.char
+  - Expected expression of type Prims.int
+    got expression 'a'
+    of type FStar.Char.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(24,12-24,15):
-  - Expected expression of type
-        Prims.int
-    got expression
-        'a'
-    of type
-        FStar.Char.char
+  - Expected expression of type Prims.int
+    got expression 'a'
+    of type FStar.Char.char
 
 >>]
 >> Got issues: [
@@ -34,32 +28,23 @@
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(43,12-43,15):
-  - Expected expression of type
-        Prims.int
-    got expression
-        'a'
-    of type
-        FStar.Char.char
+  - Expected expression of type Prims.int
+    got expression 'a'
+    of type FStar.Char.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(50,12-50,15):
-  - Expected expression of type
-        Prims.int
-    got expression
-        'a'
-    of type
-        FStar.Char.char
+  - Expected expression of type Prims.int
+    got expression 'a'
+    of type FStar.Char.char
 
 >>]
 >> Got issues: [
 * Error 189 at ExpectFailure.fst(61,12-61,15):
-  - Expected expression of type
-        Prims.int
-    got expression
-        'a'
-    of type
-        FStar.Char.char
+  - Expected expression of type Prims.int
+    got expression 'a'
+    of type FStar.Char.char
 
 >>]
 Verified module: ExpectFailure
diff --git a/tests/error-messages/IfCond.fst.expected b/tests/error-messages/IfCond.fst.expected
index ee6af5c77f3..ee49921543b 100644
--- a/tests/error-messages/IfCond.fst.expected
+++ b/tests/error-messages/IfCond.fst.expected
@@ -1,11 +1,6 @@
 >> Got issues: [
 * Error 189 at IfCond.fst(4,17-4,18):
-  - Expected expression of type
-        Prims.bool
-    got expression
-        2
-    of type
-        Prims.int
+  - Expected expression of type Prims.bool got expression 2 of type Prims.int
 
 >>]
 Verified module: IfCond
diff --git a/tests/error-messages/IfThen.fst.expected b/tests/error-messages/IfThen.fst.expected
index 2bfbf42969e..3bba48cdcdc 100644
--- a/tests/error-messages/IfThen.fst.expected
+++ b/tests/error-messages/IfThen.fst.expected
@@ -1,11 +1,6 @@
 >> Got issues: [
 * Error 189 at IfThen.fst(5,2-6,6):
-  - Expected expression of type
-        Prims.int
-    got expression
-        ()
-    of type
-        Prims.unit
+  - Expected expression of type Prims.int got expression () of type Prims.unit
 
 >>]
 Verified module: IfThen
diff --git a/tests/error-messages/NegativeTests.Neg.fst.expected b/tests/error-messages/NegativeTests.Neg.fst.expected
index 8f625813113..5603b0323a2 100644
--- a/tests/error-messages/NegativeTests.Neg.fst.expected
+++ b/tests/error-messages/NegativeTests.Neg.fst.expected
@@ -33,7 +33,7 @@
 >>]
 >> Got issues: [
 * Error 19 at NegativeTests.Neg.fst(42,33-42,34):
-  - could not prove post-condition
+  - Could not prove post-condition
   - The SMT solver could not prove the query. Use --query_stats for more details.
   - See also NegativeTests.Neg.fst(40,83-40,88)
 
diff --git a/tests/error-messages/StableErr.fst.expected b/tests/error-messages/StableErr.fst.expected
index ec93daa1465..cfffef54f96 100644
--- a/tests/error-messages/StableErr.fst.expected
+++ b/tests/error-messages/StableErr.fst.expected
@@ -1,7 +1,7 @@
 >> Got issues: [
 * Error 298 at StableErr.fst(26,0-26,20):
-  - Q = Prims.l_False
-    A query could not be solved internally, and --no_smt was given
+  - A query could not be solved internally, and --no_smt was given.
+  - Query = Prims.l_False
 
 >>]
 Verified module: StableErr
diff --git a/tests/ide/emacs/fstarmode_gh73.out.expected b/tests/ide/emacs/fstarmode_gh73.out.expected
index 01b15c320ef..0ccc0cfc801 100644
--- a/tests/ide/emacs/fstarmode_gh73.out.expected
+++ b/tests/ide/emacs/fstarmode_gh73.out.expected
@@ -1,7 +1,7 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": [{"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [135, 17], "end": [135, 24], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [136, 22], "end": [136, 29], "fname": "FStar.Reflection.V2.Formula.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Adding an implicit 'assume new' qualifier on document\n", "number": 239, "ranges": [{"beg": [36, 5], "end": [36, 13], "fname": "FStar.Stubs.Pprint.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [616, 15], "end": [616, 22], "fname": "FStar.Tactics.V2.Derived.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - FStar.Reflection.V2.Builtins.term_eq is deprecated\n  - Use FStar.Reflection.V2.TermEq.term_eq\n  - See also FStar.Reflection.V2.Builtins.fsti(149,0-149,48)\n", "number": 288, "ranges": [{"beg": [176, 11], "end": [176, 18], "fname": "FStar.Tactics.V2.Logic.fst"}, {"beg": [149, 0], "end": [149, 48], "fname": "FStar.Reflection.V2.Builtins.fsti"}]}, {"level": "warning", "message": "  - Pattern uses these theory symbols or terms that should not be in an smt pattern:  Prims.op_Subtraction\n", "number": 271, "ranges": [{"beg": [434, 8], "end": [434, 51], "fname": "FStar.UInt.fsti"}]}], "status": "success"}
-{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "  - Expected expression of type\n        int\n    got expression\n        \"A\"\n    of type\n        string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "  - Expected expression of type\n        int\n    got expression\n        \"A\"\n    of type\n        string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
+{"kind": "response", "query-id": "2", "response": [{"level": "error", "message": "  - Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "  - Expected expression of type int got expression \"A\" of type string\n", "number": 189, "ranges": [{"beg": [4, 48], "end": [4, 51], "fname": "<input>"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": [], "status": "success"}
 {"contents": {"depth": 1, "goals": [{"goal": {"label": "", "type": "bool", "witness": "(*?u[...]*) _"}, "hyps": []}], "label": "at the time of failure", "location": {"beg": [101, 12], "end": [101, 16], "fname": "FStar.Tactics.V2.Derived.fst"}, "smt-goals": [], "urgency": 1}, "kind": "message", "level": "proof-state", "query-id": "5"}
 {"kind": "response", "query-id": "5", "response": [{"level": "error", "message": "  - Tactic failed\n  - \"exact: 1 : int does not exactly solve the goal bool (witness = (*?u[...]*) _)\"\n  - See also FStar.Tactics.V2.Derived.fst(101,12-101,16)\n", "number": 228, "ranges": [{"beg": [4, 14], "end": [4, 29], "fname": "<input>"}, {"beg": [101, 12], "end": [101, 16], "fname": "FStar.Tactics.V2.Derived.fst"}]}], "status": "failure"}
diff --git a/tests/ide/emacs/integration.push-pop.out.expected b/tests/ide/emacs/integration.push-pop.out.expected
index 26f3bce803a..0c0ccbcce67 100644
--- a/tests/ide/emacs/integration.push-pop.out.expected
+++ b/tests/ide/emacs/integration.push-pop.out.expected
@@ -93,7 +93,7 @@
 {"kind": "response", "query-id": "130", "response": [], "status": "success"}
 {"kind": "response", "query-id": "133", "response": [], "status": "success"}
 {"kind": "response", "query-id": "137", "response": [{"level": "error", "message": "  - Syntax error\n", "number": 168, "ranges": [{"beg": [13, 4], "end": [13, 4], "fname": "<input>"}]}], "status": "success"}
-{"kind": "response", "query-id": "159", "response": [{"level": "error", "message": "  - Expected expression of type\n        Type0\n    got expression\n        xx\n    of type\n        nat\n", "number": 189, "ranges": [{"beg": [13, 15], "end": [13, 20], "fname": "<input>"}]}], "status": "success"}
+{"kind": "response", "query-id": "159", "response": [{"level": "error", "message": "  - Expected expression of type Type0 got expression xx of type nat\n", "number": 189, "ranges": [{"beg": [13, 15], "end": [13, 20], "fname": "<input>"}]}], "status": "success"}
 {"kind": "response", "query-id": "163", "response": [], "status": "success"}
 {"kind": "response", "query-id": "164", "response": [], "status": "success"}
 {"kind": "response", "query-id": "165", "response": [{"level": "error", "message": "  - Assertion failed\n  - The SMT solver could not prove the query. Use --query_stats for more details.\n  - See also <input>(13,15-13,23)\n", "number": 19, "ranges": [{"beg": [13, 8], "end": [13, 14], "fname": "<input>"}, {"beg": [13, 15], "end": [13, 23], "fname": "<input>"}]}], "status": "failure"}
diff --git a/ulib/FStar.FunctionalExtensionality.fsti b/ulib/FStar.FunctionalExtensionality.fsti
index 776107ce4c3..495b78b22bb 100644
--- a/ulib/FStar.FunctionalExtensionality.fsti
+++ b/ulib/FStar.FunctionalExtensionality.fsti
@@ -41,7 +41,7 @@ unfold
 let arrow (a: Type) (b: (a -> Type)) = x: a -> Tot (b x)
 
 (** Using [arrow] instead *)
-[@@ (deprecated "use arrow instead")]
+[@@ (deprecated "Use arrow instead")]
 let efun (a: Type) (b: (a -> Type)) = arrow a b
 
 (** feq #a #b f g: pointwise equality of [f] and [g] on domain [a] *)
@@ -139,7 +139,7 @@ unfold
 let arrow_g (a: Type) (b: (a -> Type)) = x: a -> GTot (b x)
 
 (** Use [arrow_g] instead *)
-[@@ (deprecated "use arrow_g instead")]
+[@@ (deprecated "Use arrow_g instead")]
 let efun_g (a: Type) (b: (a -> Type)) = arrow_g a b
 
 (** [feq_g #a #b f g]: pointwise equality of [f] and [g] on domain [a] **)
diff --git a/ulib/FStar.HyperStack.ST.fsti b/ulib/FStar.HyperStack.ST.fsti
index 1d406287a92..f2ff499b8c3 100644
--- a/ulib/FStar.HyperStack.ST.fsti
+++ b/ulib/FStar.HyperStack.ST.fsti
@@ -341,12 +341,12 @@ val salloc (#a:Type) (#rel:preorder a) (init:a)
   
 // JP, AR: these are not supported in C, and `salloc` already benefits from
 // automatic memory management.
-[@@ (deprecated "use salloc instead") ]
+[@@ (deprecated "Use salloc instead") ]
 val salloc_mm (#a:Type) (#rel:preorder a) (init:a)
   :StackInline (mmmstackref a rel) (requires (fun m -> is_stack_region (get_tip m)))
                                    (ensures  salloc_post init)
 
-[@@ (deprecated "use salloc instead") ]
+[@@ (deprecated "Use salloc instead") ]
 val sfree (#a:Type) (#rel:preorder a) (r:mmmstackref a rel)
   :StackInline unit (requires (fun m0 -> frameOf r = get_tip m0 /\ m0 `contains` r))
                     (ensures (fun m0 _ m1 -> m0 `contains` r /\ m1 == HS.free r m0))
diff --git a/ulib/FStar.Map.fsti b/ulib/FStar.Map.fsti
index 8f38448be9e..109aa14bdeb 100644
--- a/ulib/FStar.Map.fsti
+++ b/ulib/FStar.Map.fsti
@@ -183,7 +183,7 @@ val lemma_equal_elim: #key:eqtype -> #value:Type -> m1:t key value -> m2:t key v
                       Lemma (ensures (equal m1 m2 <==> m1 == m2))
                             [SMTPat (equal m1 m2)]
 
-[@@(deprecated "use lemma_equal_elim")]
+[@@(deprecated "Use lemma_equal_elim instead")]
 val lemma_equal_refl: #key:eqtype -> #value:Type -> m1:t key value -> m2:t key value ->
                       Lemma  (requires (m1 == m2))
                              (ensures  (equal m1 m2))
diff --git a/ulib/FStar.Tactics.V1.Builtins.fsti b/ulib/FStar.Tactics.V1.Builtins.fsti
index 1e2a0302850..58b4dc23bab 100644
--- a/ulib/FStar.Tactics.V1.Builtins.fsti
+++ b/ulib/FStar.Tactics.V1.Builtins.fsti
@@ -426,7 +426,7 @@ terms_, but that distinction cannot leave the Tac effect.
 
 This is only exposed as a migration path. Please use
 [Reflection.term_eq] instead. *)
-[@@deprecated "use Reflection.term_eq instead"]
+[@@deprecated "Use Reflection.term_eq instead"]
 val term_eq_old : term -> term -> Tac bool
 
 (** Runs the input tactic `f` with compat pre core setting `n`.
diff --git a/ulib/FStar.Tactics.V2.Builtins.fsti b/ulib/FStar.Tactics.V2.Builtins.fsti
index caa2a823683..82a8c19e388 100644
--- a/ulib/FStar.Tactics.V2.Builtins.fsti
+++ b/ulib/FStar.Tactics.V2.Builtins.fsti
@@ -413,7 +413,7 @@ terms_, but that distinction cannot leave the Tac effect.
 
 This is only exposed as a migration path. Please use
 [Reflection.term_eq] instead. *)
-[@@deprecated "use Reflection.term_eq instead"]
+[@@deprecated "Use Reflection.term_eq instead"]
 val term_eq_old : term -> term -> Tac bool
 
 (** Runs the input tactic `f` with compat pre core setting `n`.
diff --git a/ulib/prims.fst b/ulib/prims.fst
index 90025867937..cf210ae3bda 100644
--- a/ulib/prims.fst
+++ b/ulib/prims.fst
@@ -616,32 +616,32 @@ let as_ensures (#a: Type) (wp: pure_wp a) : pure_post a = fun (x:a) -> ~(wp (fun
 (** The keyword term-level keyword [assume] is desugared to [_assume].
     It explicitly provides an escape hatch to assume a given property
     [p]. *)
-[@@ warn_on_use "uses an axiom"]
+[@@ warn_on_use "Uses an axiom"]
 assume
 val _assume (p: Type) : Pure unit (requires (True)) (ensures (fun x -> p))
 
 (** [admit] is another escape hatch: It discards the continuation and
     returns a value of any type *)
-[@@ warn_on_use "uses an axiom"]
+[@@ warn_on_use "Uses an axiom"]
 assume
 val admit: #a: Type -> unit -> Admit a
 
 (** [magic] is another escape hatch: It retains the continuation but
     returns a value of any type *)
-[@@ warn_on_use "uses an axiom"]
+[@@ warn_on_use "Uses an axiom"]
 assume
 val magic: #a: Type -> unit -> Tot a
 
 (** [unsafe_coerce] is another escape hatch: It coerces an [a] to a
     [b].  *)
-[@@ warn_on_use "uses an axiom"]
+[@@ warn_on_use "Uses an axiom"]
 irreducible
 let unsafe_coerce (#a #b: Type) (x: a) : b =
   admit ();
   x
 
 (** [admitP]: TODO: Unused ... remove? *)
-[@@ warn_on_use "uses an axiom"]
+[@@ warn_on_use "Uses an axiom"]
 assume
 val admitP (p: Type) : Pure unit True (fun x -> p)