pretty-printer: consistently print nested tuples with (,) syntax

src/parser/FStar.Parser.ToDocument.fst

@@ -1990,9 +1990,10 @@ and p_appTerm e = match e.tm with
         group (soft_surround_map_or_flow 2 0 head_doc (head_doc ^^ space) break1 empty p_argTerm args)
       )
 
-  (* (explicit) dependent tuples are handled below *)
+  (* (explicit) tuples and dependent tuples are handled below *)
   | Construct (lid, args) when is_general_construction e
-        && not (is_dtuple_constructor lid && all1_explicit args) ->
+        && not (is_dtuple_constructor lid && all1_explicit args)
+        && not (is_tuple_constructor  lid && all1_explicit args) ->
     begin match args with
       | [] -> p_quident lid
       | [arg] -> group (p_quident lid ^/^ p_argTerm arg)
@@ -2074,6 +2075,8 @@ and p_atomicTermNotQUident e = match e.tm with
       surround 2 1 (lparen ^^ bar)
         (separate_map (comma ^^ break1) (fun (e, _) -> p_tmEq e) args)
                    (bar ^^ rparen)
+  | Construct (lid, args) when is_tuple_constructor lid && all1_explicit args ->
+      parens (p_tmTuple e)
   | Project (e, lid) ->
     group (prefix 2 0 (p_atomicTermNotQUident e)  (dot ^^ p_qlident lid))
   | _ ->

tests/error-messages/Bug3099.fst

@@ -0,0 +1,11 @@
+(* Test case: nested tuples print strangely in tactic dumps.
+  They look OK with --print_in_place though.
+  (This isn't strictly an error message test, but it is testing debug
+  messages, which are important too.)
+*)
+module Bug3099
+
+module Tac = FStar.Tactics
+
+let check_print_tuples () =
+  assert ((1, (2, (3, 4))) = (1, (2, (3, 4)))) by (Tac.dump "X")

tests/error-messages/Bug3099.fst.expected

@@ -0,0 +1,7 @@
+proof-state: State dump @ depth 0 (X):
+Location: Bug3099.fst(11,50-11,64)
+Goal 1/1:
+(_: Prims.unit), (return_val: Prims.eqtype), (_: return_val == Prims.int * Prims.int * Prims.int * Prims.int), (any_result: Prims.bool), (_: true == any_result), (any_result'0: Prims.logical), (_: Prims.l_True == any_result'0) |- _ : Prims.squash ((1, (2, (3, 4))) = (1, (2, (3, 4))))
+
+Verified module: Bug3099
+All verification conditions discharged successfully