Fix two bugs related to printing projections in smtv2 printer.
In the printer:
- in the task, forbid projections of sum types (i.e., only allow them in records)
- generate and remember missing projection names when declaring data types
- pattern matching data types : use the remembered projections
In eliminate_algebraic_if_poly:
- When in the non-polymorphic case, eliminate projections of non-record types.
This should fix #644 (closed) and #725 (closed)