primproj: warning and avoid error.

When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.

0 files changed, 0 insertions, 0 deletions