More on "match" in primitive records.

text/primitive-projections.md

@@ -43,10 +43,12 @@ See associated [Zulip discussion](https://coq.zulipchat.com/#narrow/stream/23765
 
 ## Issue 3: the status of `match` and destructing `let` in "primitive" record types
 
-See e.g. [#13913](https://github.com/coq/coq/pull/13913).
+See impact of desugaring `match` in terms of complexity ([#13913](https://github.com/coq/coq/pull/13913)) or unification ([#6726](https://github.com/coq/coq/issues/6726), [9763](https://github.com/coq/coq/issues/9763)) or readability ([6723](https://github.com/coq/coq/issues/6723)).
 
 *Design choice 1*: keep `match` nodes as they are in primitive record types; they will behave correctly for reduction (that is like their expansion into projections); to deal with them in the conversion, it is enough to extend the conversion with eta-expansions of `match` into projections.
 
+*Design choice 2*: forbid `match` at all on primitive record types (as well as `fun 'pat => ...` and `let 'pat := ... in ...` and `let (x1,...,xn) := ... in ...`), even as a primitive form of sugar, making primitive and non-primitive record types two incompatible styles of formalization.
+
 ## Issue 4: The status of the `t.(f args)` notation as an alternative notation for any kind of application.
 
 See e.g. [#11332](https://github.com/coq/coq/pull/11332).