All: replace all uses of * for tuples by &

[mtzguido]

This patch automatically generated by adding this patch to ToSyntax.fst:

diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
index e0ddf1b9a4..aeb75732db 100644
--- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
+++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst
@@ -1173,13 +1173,25 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an
     | Op(op_star, [lhs;rhs]) when
       (Ident.string_of_id op_star = "*" &&
	op_as_term env 2 op_star |> Option.isNone) ->
-      (* See the comment in parse.mly to understand why this implicitly relies
-       * on the presence of a Paren node in the AST. *)
+      (* See the comment in parse.mly to understand why this implicitly relies *)
+      (* on the presence of a Paren node in the AST. *)
+      let print1 (op:ident) : unit =
+        let open FStar.Compiler.Range in
+        let open FStar.Class.Show in
+        let r = range_of_id op in
+        BU.print3 "GGG %s %s %s\n"
+          (file_of_range r |> BU.normalize_file_path)
+          (start_of_range r |> line_of_pos |> show)
+          (start_of_range r |> col_of_pos |> show)
+      in
+      print1 op_star;
+
       let rec flatten t = match t.tm with
	 // * is left-associative
	 | Op(id, [t1;t2]) when
	    string_of_id id = "*" &&
	    op_as_term env 2 op_star |> Option.isNone ->
+          print1 id;
	   flatten t1 @ [ t2 ]
	 | _ -> [t]
       in

And using the following scripts:

fix_all.sh:

#/bin/bash
set -eux

IFS=" "
while read marker file line col; do
	if [ "x${marker}" != "xGGG" ]; then
		continue;
	fi
	./fix1.sh "${file}" "${line}" "${col}"
done

fix1.sh:

#/bin/bash
FILE=$1
LINE=$2
COL=$3

sed -i "${LINE}s/^\(.\{${COL}\}\)\*/\1\&/" ${FILE}

Then by running make ci | tee L we save all positions where * was resolved to tuples, and can run grep GGG L | ./fix_all.sh to automatically fix all of them.

This patch does not cause a snapshot diff, which is a good sign!

A single use of a non-dependent tuple with a refinement on the left needed a tweak (ValidatedAccess.fst), adding parenthesis as in #3317.